Proofs are Programs: 19th Century Logic and 21st Century Computing

Proofs are Programs: 19th Century Logic and 21st Century Computing

As the 19th century drew to a close, logicians formalized an ideal notion of proof. They were driven by nothing other than an abiding interest in truth, and their proofs were as ethereal as the mind of God. Yet within decades these mathematical abstractions were realized by the hand of man, in the digital stored-program computer. How it came to be recognized that proofs and programs are the same thing is a story that spans a century, a chase with as many twists and turns as a thriller. At the end of the story is a new principle for designing programming languages that will guide computers into the 21st century.

This paper by Philip Wadler was a Dr Dobbs article in 2000 and has a matching a Netcast interview.

This nifty paper starts with Frege's Begriffschrift in 1879 and goes to Gentzen's sequent calculus, Church's untyped and then typed lambda calculus, and then brings it all together to describe the Curry-Howard correspondence. For the grand finale, Wadler connects this to Theorem Provers and Proof Carrying Code and gives commercial examples where it all pays off.
This is an enjoyable story and a fun introduction to type theory and the Curry-Howard correspondence.

For more of Wadler's writings along these lines check out his History of Logic and Programming Languages paper collection.

edit: fixed the dr dobbs article link

Comment viewing options

Uncool URLs

The link didn't work for me. Seems like you need to search for wadler, and follow the link from the results page.

Fixed!

Found and fixed the link.

This is a very good

This is a very good introduction to Curry-Howard. I am certain it was mentioned here many times before, but one more time wouldn't hurt, I guess..

Couldn't find it, thus I posted.

I checked via the search box and google before posting the story, and could only find one mention of this paper in a comment.
Since I had so much fun reading it, I figured I'd post it.

That's the right decision,

That's the right decision, of course :-)

A slightly OT question

I'd like to know if any of you guys know of any good popular scientific book describing the history of computer science, perhaps along the lines of Wadler's paper. I've been searching for this for quite a while and the only thing that comes close is Martin Davis' book "Engines of logic". But as you can guess from the title he ends up talking about computers and computer engineering instead of computer science.

Why am I interested in this? I find that people in general have no idea what computer science is about. Whenever I say that I'm a Ph.D. student in computer science people reply: "Oh, computers and stuff!". To which I have to reply "No, more like programming and studying computations." At which point I've already lost them. One thing that I hope could help this situation is a really good popular scientific book about computer science. But I have yet to find one. I guess I'll have to write one myself. Just got to finish that thesis first...

This might work for you. I

This might work for you. I have my issues with this book, but it's better than many others. I too think the ultimate book about this is yet to be written. Perhaps we should all get together one weekend (with plenty of beer) and get it over with...

Thanks

Thanks for your link to the book. I'll be sure to read it some time. Though having the title begin with "Algorithmics" will surely scare off a lot of people.

Working together on trying to brainstorm at least an embroy of a book would be a lot of fun. I had another idea about trying to write the book collaboratively over the net. But I'm not very good at organizing things so I tend to put off these kind of thoughts.

We use that book at the

We use that book at the introduction course to computer science here in Lund.

Perhaps also 'Computers Ltd'?

I was struggling to write a section on why programs can't be derived automatically from their specification, and was pointed at "Computers Ltd - What they really can't do" by David Harel for inspiration. It's definitely in the 'popular science' category.

I can't actually recommend it (yet?), because I've only briefly flicked through bits of it so far...

Computers Ltd

Thanks! As is turns out the book you suggest is written by the same author as the book Ehud suggested. This guy Harel seems to be the man when it comes to popularising computer science. I found another book by him called "The Science of Computing: Exploring the Nature and Power of Algorithms" which seems to be about pretty much the same thing as the other two books.

Anyway, I will definitely read one of Harel's books.

Datics - The Physics of Data

As you say, people think they know what Computer Science means, so I sometimes use a different made up word to break out of the stereotype.
I say I study datics, the physics of data.
Then I get to talk about paradoxes, equations, the Curry-Howard correspondence and that sort of cool stuff.

Hmmm...

Hmmmm... Your idea is good but I'm wary of using non-standard terminology. I've been trying to use the swedish term "BerÃ¤kningsvetenskap" (which translates to computING science) and that's about as far as I have dared to go outside the field of established terminology. But maybe I should give "datics" a try. It doesn't translate that well into swedish though...

Informatics

The german word for computer science is "Informatik", which isn't too bad, being a bit more general and abstract. I believe something equivalent to "informatics" is also used in some other countries/languages.

Kristen Nygaard...

..., of Simula fame, tried to promote "informatics" long ago (Program Development as a Social Activity)

The term "computer science" should be replaced by "informatics". Some years ago the choice between the two terms seemed perhaps to be of little consequence. Discussions of terminology often are idle, but they may some times reflect basic differences of opinion or at least emphasis. Today it is unfortunate that the term "computer science" is used. The term tends to implant a too narrow way of thinking about information systems, that now are networks of people, information processing equipment and other machinery, interacting through direct interhuman and (an increasing proportion of) electronically supported communication links..... Informatics is the science that has as its domain information processes and related phenomena in artifacts, society and nature.

Informatics

In swedish we use both "datavetenskap" and "informatik". But I'm afraid that the term "informatik" is no more useful than "datavetenskap". AFAIK most people have absolutely no idea what "informatik" is, they won't even associate to computers. Hence my wish to educate the masses a bit.

AFAIK most people have

AFAIK most people have absolutely no idea what "informatik" is, they won't even associate to computers.

That's slightly different in Germany: indeed most people have no idea what "Informatik" is, but that's because everybody is associating it only with computers... ;-) In other words, the choice of word did not have the desired effect either.

Computers and stuff

I think their reply is fine. It's an approriate level of abstraction for their interest in what you do.

Feynman the Explainer

Sorry to reply to my own post, but this thread just reminded me of a nice article I read on Richard Feynman and his work at Thinking Machines. There's a section of that page with the heading "Feynman the Explainer". Here's a quote:

We tried to take advantage of Richard's talent for clarity by getting him to critique the technical presentations that we made in our product introductions. Before the commercial announcement of the Connection Machine CM-1 and all of our future products, Richard would give a sentence-by-sentence critique of the planned presentation. "Don't say reflected acoustic wave.' Say echo." Or, "Forget all that local minima' stuff. Just say there's a bubble caught in the crystal and you have to shake it out." Nothing made him angrier than making something simple sound complicated.

Brains and stuff

I don't think it's all that appropriate, it simply reflects the general lack of awareness of the subject. If you tell someone you're a psychologist, they usually know better than to respond, oh, brains and stuff!

Psychology...

Psychology... that's like psychiatry, isn't it? :)

software

I usually tell people that it's about software. That's a word that people have some intuition for.

Software

Doesn't "software" give the wrong connotations? I'm afraid they'll start thinking about Word and Internet Explorer and then they will start asking me if I can help them get this or that program to run on their computer.

I'm sorry if I sound a little bitter here. It's just that I've been asked so many time to do things that I can't do just because people have gotten the wrong impression about what it is that I work with. And I'm getting tired of it. That's why I'm picky about the connotations.

If asked to do something you

If asked to do something you can't do then politely tell them that it is not your area of expertise. Even if they knew what you did, it wouldn't be unreasonable for them to ask, since many people in "computer science" are familiar with day to day operations of the computer.

Personally, I have accepted that for most people computers are a black box that runs their applications. When people ask what I do I say I "work with computers", and that seems to satisfy them.

Your reaction to me seems overly sensitive and unrealistic. I mean, you want to write a book to educate the masses, so that when somebody asks what you do you'll say "here, read this book"?

When I'm asked what I do...

...I just tell them I'm a contributing editor for Lambda-the-Ultimate. :-)

The root of the problem

You seem to draw an awful lot of conclusions based on very little information.

I DO tell people politely that some computer related things are not in the area of my expertise. What I did in my previous post was just to let off some frustration. I'm normally a very friendly guy IRL. And you're of course right in that it is reasonable to expect of me to know a bit about computers. What I was hoping to avoid was using a term that would encourage people even more to draw false conclusions about my area of expertise. I think that is in the interest for all.

Therefore I personally wouldn't say that I "work with computers" just as an astronomer wouldn't say that he "works with telescopes". It focuses on the tool rather than the task and is in my opinion simply misleading. But it might not be misleading in your case of course.

And no, I don't intend to hand people a book every time somebody asks me what I do. Instead I'm hoping to come to the root of the problem that people in general seem, at least in my experience, ignorant about computer science. One way of doing that might be to wright good popular scientific books about computer science. I haven't seen such books myself and thus I just wanted to know if anyone else had.

This, of couse, refers to

This, of couse, refers to Dijkstra's quote Computer science is no more about computers than astronomy is about tlescopes, which should go on your T-shirt instead of the misleading "techincal fellow" description...

I, for one, understand your frustration. I also think that popularization is, in general, A Good Thing.

You're absolutely right

You're absolutely right. I guess it wouldn't have hurt if I had acknowledged Edsger Dijkstra. And speaking of t-shirt I found a site which sells t-shirts with Dijkstra quotes. If it weren't for the fact that I'm really short on money right now I'd definitely buy one. Or two. The following quote would also be nice to wear:

The question of whether a computer can think is no more interesting than the question of whether a submarine can swim.

one of my favorite possessions...

is a T-Shirt that says "No, I won't fix your computer". I don't have to wear it to work often, but word manages to get around that "Technology Fellow" means something different than "guy who knows how to configure Outlook".

Easy!

"Paul, what do you do?"

"I write software. Well, nowadays I'm one of those horrible middle managers, which means that I talk about writing software."

<knowing_laugh/>

heh

The other day my daughter bought homework which consisted on drawing mama and papa on their jobs. Well, we -- it's never just *her* homework -- decided to draw me on the keyboard, just in front of the monitor. But thinking about it now, I guess the teatcher may believe i'm just an unemployed surfing the web all day long... :P

really hard to describe what a software developer does...

What a software developer does

When, as a child, I used to ask my dad (a programmer) what he does all day, he always replied "scribbling on bits of paper, screwing them up and throwing them away". That was punched-card days; now we scribble in emacs windows, I guess.

Yes...

...the transition from punch cards to glass ttys has had the principal benefit of making it easier to hide our mistakes! :-)

The interactions of applied mathematics and logic.

I'm not qualified to write it, but if the eminances here actually agreed on the contents of such a manuscript, I'd pay for it without hesitation.

The appendix on static vs. dynamic vs. strong vs. weak typing might end up being a few hundred pages though. :-)

(ed: oops, was supposed to be in reply to Mr. Ehud's comment about getting together to write one.)

When we manage to set up the

When we manage to set up the LtU-wiki we might try to come up with something...

Pattern on the Stone

How about the Pattern on the Stone?
An easy read for sure.
Amazon

mp3

I never managed to download the mp3 file. Did you?

Yes

I tried again, and the FTP server seems empty. But you can just download the 'stream' version: http://media.cmpnet.com/technetcast/wadler.mp3 (wget worked for me).

The quality is mediocre, the interview seems to be taken over the phone.

cheers!