 A Practical Theory of Programming
started 4/28/2004; 2:48:08 AM - last post 4/29/2004; 4:59:35 AM
|
|
Ehud Lamm - A Practical Theory of Programming 
4/28/2004; 2:48:08 AM (reads: 24854, responses: 2)
|
|
| A Practical Theory of Programming |
|
E.C.R.Hehner, a Practical Theory of Programming,
second edition, 2004 January 1.
The book, originally published by Springer-Verlag in 1993 is now online.
I haven't read it, but it looks rather intriguing (check, for example, section 5.7 on Probabilistic Programming).
If anyone is more familiar with the book, I'd be glad to hear what you think.
Posted to Misc-Books by Ehud Lamm on 4/28/04; 2:50:21 AM
|
|
|
|
graydon hoare - Re: A Practical Theory of Programming
4/28/2004; 10:24:42 AM (reads: 677, responses: 0)
|
|
|
I have read this book, and have taken a course with Hehner. I believe his work is a great overlooked corner of the field; it builds a practical refinement calculus in which the "final" terms are machine instructions, and in which the refinement relation is logical implication. there is therefore no "program / proof duality" as in many refinement calculi; the final program in machine code is a logical term which directly implies its specification, in the theory.
it is unclear whether any user interface might be developed to make such an approach pleasant for the practitioner; any more pleasant than say operating a proof assistant. yet with the possible exception of ACL2, which is designed in the same spirit as aPToP, even proof assistants maintain this terrible division in terms, such that the "program extraction" phase is a painful and tedious matching up of terms. this book provides a clear vision of how much is to be gained from treating machine state and machine instructions as fundamental logical terms; and moreover how computer scientists should not be afraid to design a logic which works best for such terms.
Hehner has a unique talent for writing blunt, simple explanations of concepts which are usually presented in a big mess. his "math advice" paper would have saved me years of agony in highschool. his "unified algebra" paper presents an exciting, constructive way forward for logic, math and computer scienence. I would recommend reading all his papers; each one has given me a great deal of ideas, as well as hope that math and CS might someday get cleaned up.
|
|
Andris Birkmanis - Re: A Practical Theory of Programming
4/29/2004; 4:59:35 AM (reads: 505, responses: 0)
|
|
|
I enjoyed the book so far (I am at 5.2.4 at the moment), despite the lack of attention to continuations:
The trouble with go to is that it cannot be considered a specification, and it does not refine any specification. It does not fit in any usable theory of programming.
And all this just one page after dealing with loops with exits!
Let me suggest Declarative Continuations and Categorical Duality as a complementary reading to this book. The main value for me was an idea of giving denotational semantics in CPS, which enables describing evaluation strategy, non-local exits, and other "troublesome" features precisely. The paper is pretty old, so if anybody suggests anything more recent, I will be grateful.
|
|
|
|