4 ms·

Where and how can one effectively learn the kind of formal reasoning he describes, and that he mentions having taught to college freshmen? Could a knowledgeabl

by limist 16y ago

Where and how can one effectively learn the kind of formal reasoning he describes, and that he mentions having taught to college freshmen? Could a knowledgeable HN'er please give follow-up resources? Thanks!

arethuza 16y ago
You might want to look at something like: http://en.wikipedia.org/wiki/Formal_semantics_of_programming_languages http://en.wikipedia.org/wiki/Formal_semantics_of_programming... I seem to remember that Dijkstra was keen on identifying weakest preconditions of different statements that can be used to prove a program correct. However, I warn you that if you try this you will soon find out what this kind of formal reasoning about programs never caught on that widely - at least for imperative programs.
jhck 16y ago
I was introduced to formal reasoning about programs in an introductory course on algorithms and data structures in March. Most of the curriculum was from CLRS,[1] which presents proofs of correctness for many algorithms but doesn't explain how to develop such proofs. The curriculum for the last two weeks of the course, however, was a handout titled Transition Systems,[2] which I found to be an excellent introduction to the subject. Since that time I've been interested in the idea of proving programs correct. On weekends I'm currently making my way through David Gries's The Science of Programming. Similar books include - A Discipline of Programming by Dijkstra - The Evolution of Programs by N. Dershowitz [1] http://mitpress.mit.edu/algorithms/ http://mitpress.mit.edu/algorithms/ [2] http://www.cs.au.dk/dADS1/daimi-fn64.pdf http://www.cs.au.dk/dADS1/daimi-fn64.pdf
- drothlis 16y ago
  In a similar vein is Elements of Programming by Alexander Stepanov (designer of the C++ STL) and Paul McJones: http://www.elementsofprogramming.com/book.html http://www.elementsofprogramming.com/book.html
  - limist 16y ago
    @jhck, drothlis: Thank you very much to both of you, those suggestions are exactly what was asked for. I'd upvote you more if I could. :) Both the Gries book and Stepanov's book have really impressive reviews on Amazon, am looking forward to diving into them. http://www.amazon.com/Science-Programming-Monographs-Computer/dp/0387964800 http://www.amazon.com/Science-Programming-Monographs-Compute... http://www.amazon.com/Elements-Programming-Alexander-Stepanov/dp/032163537X/ http://www.amazon.com/Elements-Programming-Alexander-Stepano...
Dn_Ab 16y ago
I think category theory could be the maths for software engineers to the mechanical engineers calculus. Once you get past the arrows and weird Greek nomenclature you realize its just algebra. It seems a reasonable compromise to using formal logic whose cost is simply not worth it in most all cases. Still most presentations are very academic and neither presented in the way that a busy engineer can easily grasp and use. I've been trying to simultaneously learn and break it down to a much simpler core for my self that can be used without thinking - kind of like how engineers use physics - but still serve as a strong scaffolding of support when attacking a problem. Progress is tough though.

by limist 16y ago

arethuza 16y ago

You might want to look at something like: http://en.wikipedia.org/wiki/Formal_semantics_of_programming_languages http://en.wikipedia.org/wiki/Formal_semantics_of_programming... I seem to remember that Dijkstra was keen on identifying weakest preconditions of different statements that can be used to prove a program correct. However, I warn you that if you try this you will soon find out what this kind of formal reasoning about programs never caught on that widely - at least for imperative programs.

jhck 16y ago

I was introduced to formal reasoning about programs in an introductory course on algorithms and data structures in March. Most of the curriculum was from CLRS,[1] which presents proofs of correctness for many algorithms but doesn't explain how to develop such proofs. The curriculum for the last two weeks of the course, however, was a handout titled Transition Systems,[2] which I found to be an excellent introduction to the subject. Since that time I've been interested in the idea of proving programs correct. On weekends I'm currently making my way through David Gries's The Science of Programming. Similar books include - A Discipline of Programming by Dijkstra - The Evolution of Programs by N. Dershowitz [1] http://mitpress.mit.edu/algorithms/ http://mitpress.mit.edu/algorithms/ [2] http://www.cs.au.dk/dADS1/daimi-fn64.pdf http://www.cs.au.dk/dADS1/daimi-fn64.pdf

drothlis 16y ago
In a similar vein is Elements of Programming by Alexander Stepanov (designer of the C++ STL) and Paul McJones: http://www.elementsofprogramming.com/book.html http://www.elementsofprogramming.com/book.html
- limist 16y ago
  @jhck, drothlis: Thank you very much to both of you, those suggestions are exactly what was asked for. I'd upvote you more if I could. :) Both the Gries book and Stepanov's book have really impressive reviews on Amazon, am looking forward to diving into them. http://www.amazon.com/Science-Programming-Monographs-Computer/dp/0387964800 http://www.amazon.com/Science-Programming-Monographs-Compute... http://www.amazon.com/Elements-Programming-Alexander-Stepanov/dp/032163537X/ http://www.amazon.com/Elements-Programming-Alexander-Stepano...

Dn_Ab 16y ago

I think category theory could be the maths for software engineers to the mechanical engineers calculus. Once you get past the arrows and weird Greek nomenclature you realize its just algebra. It seems a reasonable compromise to using formal logic whose cost is simply not worth it in most all cases. Still most presentations are very academic and neither presented in the way that a busy engineer can easily grasp and use. I've been trying to simultaneously learn and break it down to a much simpler core for my self that can be used without thinking - kind of like how engineers use physics - but still serve as a strong scaffolding of support when attacking a problem. Progress is tough though.