Predicate calculus and program semantics

What Hacker News says

1. User23Mar 2024
   This[1] contains an explanation of his proof format. More generally many of the later monographs from that archive have interesting proofs. Also the book Predicate Calculus and Program Semantics is chock full of proofs.

   [1] https://www.cs.utexas.edu/users/EWD/transcriptions/EWD13xx/E...

   thread
2. User23Dec 2023
   Well it's not popular (even though it ought to be), but Edsger Dijkstra's A Discipline of Programming is an approachable and informal (by the author's standards) look at solving non-trivial problems in a provably correct way. In fact the entire EWD archive[1] can be arranged into a course pretty readily, although you'll definitely want to skim or skip large chunks of it. Also some of the papers are just acerbic observations on life, which some people like and some don't.

   And there's it's big brother Predicate Calculus and Program Semantics by Dijkstra and Scholten that more rigorously formalizes the same approach.

   Dafny[2] is one approach out of Microsoft Research that attempts to provide automated tooling around some of those concepts.

   All of the above are excellent places to start if you're interested in learning how to write better code with the imperative languages that you're actually going to use professionally.

   [1] https://www.cs.utexas.edu/users/EWD/

   [2] https://dafny.org/

   Show morethread
3. User23Sep 2022
   Dijkstra’s A Discipline of Programming and its spiritual successor that he did with Scholten Predicate Calculus and Program Semantics. They changed how I think about programming.
   thread
4. User23Nov 2021
   It sounds like you might appreciate Predicate Calculus and Program Semantics[1] which is a rigorous formal treatment of the subject. Dijkstra's earlier work, A Discipline of Programming[2] lacks mathematical rigor, but is still quite pragmatic and is arguably a much gentler introduction to the subject. It also focuses more on real-world use cases.

   Like most of his work, the general theme is "how can we avoid making a mess of things unnecessarily?" Avoiding needless complexity is clearly the programmer's greatest challenge.

   [1] https://www.goodreads.com/book/show/3144463-predicate-calcul...

   [2] https://www.goodreads.com/book/show/2276288.A_Discipline_of_...

   Show morethread
5. User23Jul 2021
   > The key insight of Dijkstra is that we should use a kind of substitution calculus to derive programs from invariants.

   It baffles me that the "formal methods" (it really should be called automated methods) crowd not only ignores this lesson, but is completely blind to it. In my direct experience, the ones I've spoken to are so obsessed with verification that the idea of constructing a program that has specified properties apparently isn't even thinkable for them. Perhaps it's a defect in my ability to explain things, but I've never once managed to explain to one of them that construction is a significantly easier task than verification. It's a real shame because they're very intelligent people that I'm certain could contribute greatly to formal program derivation. I suppose it's one of those "professional deformations" Dijkstra occasionally mentions. One of the things I'd like to do when I have copious free time is build an Emacs mode that only allows edits that preserve the given invariants, perhaps using TLA+ or something similar.

   Anyone that wants to learn more on the subject of deriving programs should read one or both of A Discipline of Programming[1] and Predicate Calculus and Program Semantics[2]. The former is more approachable for the programmer who isn't as inclined toward formal mathematics. The latter basically takes the same concepts and treats them with much greater mathematical rigor.

   [1] https://www.goodreads.com/book/show/2276288.A_Discipline_of_...

   [2] https://www.goodreads.com/book/show/3144463-predicate-calcul...

   Show morethread
6. User23Jun 2020
   The predicate calculus. I regularly review Predicate Calculus and Program Semantics[1] to increase my fluency in the techniques. I also recommend A Discipline of Programming[2] as a gentler introduction to the subject for those who do not consider themselves particularly mathematically inclined. For me it was a natural progression from doing TDD. I still code test first, but now the structure of those tests and programs is guided by a better understanding of program semantics, greatly increasing my code quality.

   [1] https://www.amazon.com/Predicate-Calculus-Semantics-Monograp...

   [2] https://www.amazon.com/Discipline-Programming-Edsger-W-Dijks...

   Show morethread