CMSC 838Y Paper Reviews

Skip down to paper 0: Philip Wadler. Proofs are programs: 19th century logic and 21st century computing, November 2000. Appeared in Dr. Dobbs Journal as 'New Languages, Old Logic' in December 2000. [ .pdf ]

Reviews for paper 0

Review from Mike Hicks <> at Tue Feb 4 22:19:03 EST 2003:

This is a really cool paper.  That correspondence is really something!

Review from Yuan Yuan > yuanyuan@cs> at Sat Feb 8 11:26:25 EST 2003:

Paper review: Proofs are Programs

This paper is written in a quite readable and interesting way. Using a few 
symbols and detailed narration, it draws out a picture to illustrate essences 
of natural deduction and lambda calculus and their correspondences. And now 
these principles are bases and guides for designing programming languages and 
especially type system in these languages. The conclusion of the paper gives 
extensive examples how programming languages exploiting the principles in 
different way. Thus, the paper is a good introductory paper for us to explore 
more in direction of refining and designing theorem provers, solving code 
security problem and so on, though there is no much new idea in this paper.

After reading this paper, I knew the evolution of Gentzení»s natural deduction 
and the lambda calculus and typed lambda calculus more clearly. So 
understanding why proofs are programs is easier. It is interesting to see how 
computing universe can be built from just three term forms and one reduction 
rule. The merit of this paper are summarizing them out, explaining then clearly 
and showing examples. Hm.. I do not see anything redundant in this paper as a 
narration paper. 

Review from Bryan Payne <bdpayne@cs> at Sun Feb 9 13:17:12 EST 2003:

This paper set out to show (as the title implies) how proofs and programs can 
be viewed as the same thing.  To this end, the paper does a resonablly good 
job.  However, it would have been nice to see the case made a little more 
concrete.  The two major points made in support of this argument seem to be the 
extreme flexability of lambda calculus and the ability to use formal proofs for 
type checking.  Certainly these ideas do take us a long way, but perhaps I was 
looking for a cleaner, 1 to 1 mapping between the two paradigms.  In 
retrospect, this likely isn't achievable.  And, if it is, it would take much 
more discussion than the 15 pages of this paper.

Having said that, I really enjoyed reading this paper.  For me, it did so much 
more than just explain how proofs are programs.  The historial background on 
lambda calculus and type systems was very well written and provided a lot of 
insight into the conveluted notation that we use today.  In addition, the 
discussion of typed lambda calculus took a topic that is full of complex 
notation and described it in a clean and precise maner.  Perhaps this paper 
should be made mandatory for systems folk like myself (i.e., those who last 
touched lambda calculus over 7 years ago).

While the historical background about lamba calculus was certainly interesting, 
my favorite part of this paper was the conclusion.  As someone who works in the 
field of security research, I took great interest in seeing the connections 
being drawn between typed langugages and security.  Specifically, the 
discussion on proof carrying code presented some interesting research areas of 
great importance to a person like me.

Overall, I felt that the paper was well written and presented the material in a 
very approachable fashion.

Review from Polyvios Pratikakis <polyvios@cs> at Tue Feb 11 04:22:52 EST 2003:

This paper can be an introductory reading for fields such as lambda calculus, 
logic, type systems or computational models. Written in an "easy-digestable" 
way, it starts with an introduction of formal logic and lambda calculus, 
augmented with historical facts. After that, the author presents typed 
lambda-calculus as a small introduction to type-systems, and refers to the 
correspondence of lambda calculus and Gentzen's logic system. Enriched with 
many historical (but still interesting) references, the paper presents the 
still-ongoing correspondance between mathematical logic and computation 
models/programming languages. Concluding, there is a wide reference to 
(functional) programming languages, since their beginning with lisp. Most past 
and current functional languages are mentioned, and the fact that many 
successful theorem provers are written in functional languages is stressed 
The issue of safety and type-checking as a safety tool is discussed towards the 
end of the paper, and proposed solutions for safety are presented. This is the 
only part of the paper that non-functional languages are mentioned (Java, C, 
C++, Modula-3, TAL, etc), to stress the fact that even non-fuctional languages' 
typesystems correspond to theorem-proofs in mathematical logic.
Overall, it is a well-written paper, that presents in an intuitive way the 
correspondence between formal proofs and computer programs/typesystems.
It succeeds in inciting the reader's curiosity on the type-systems' field, and 
contains many references, both historical and current, mathematical and 
application-oriented. The only thing missing is a formal list of references in 
the end, that would forward the reader to more technical/formal readings, 
although they are referenced in the text.

Review from at Tue Feb 11 11:44:56 EST 2003:

This paper  gives the realtionship between the logic and the stored program 
computer.This paper explains the Gentzen's natural deduction and Church's 
lambda calculus.In the early part of the paper author describes the theory 
behid the Gentzen's natural deduction and church's lambda Calculus.The 
Gentzen's natural system has structural and logical rules.This paper also 
highlights the subforula property of the Gentzen's paper.Gentzen presents the 
various ways of formatting logic,natural deduction and sequent calculus.
Church's lambda brings the concep of the typed systems.Functional programing 
and types are used used in almost all the languages.

In the later section of the paper the auther explians the concept of Theorem 
provers and Proof Carrying Code.Types ensure the security.According to the 
paper the types are checked before running which is economical.There is a 
desciption of the difference of the type checkers of Java and TAL.

In the end of the paper PCC 's advantageas and disadvantages are 
mentioned.Unlike TAL ,instead of adding types to the machine code one adds the 
proof directly.Example of PCC are packet filters Java.

so in short Proofs are Programs.

Review from James Rose <rosejr@cs> at Tue Feb 11 12:10:34 EST 2003:

	The heart of this paper is the Curry-Howard correspondance,
and it presents this in a clear manner, with good historical
background and examples.  Papers such as this one, which do not
contribute new results, but instead frame and link together past
research, must obviously be evaluated by different criteria than
articles on new or ongoing research.  Clarity and interest are perhaps
two of the primary criteria.  On the first I have no complaints; the
color used in the type derivation aids comprehension, and the gradual
development is easy to follow, yet still surprising when the
fundamental result is revealed.  Correspondences like this are almost
always of interest, as they help to distill ideas down to their
essences.  Understanding that proofs and programs are the same helps
us to understand what they really do.  The primary thing that I think
could improve this paper is a list of references.  The conclusions
section lists many interesting consequences and related work, but
doesn't tell you where to go to find more about it.  I assume this was
done because each subject mentioned spans many papers and giving just
one would not be representative.

Generated: Thu Mar 6 15:39:24 EST 2003 by mwh