Program Proofs

What Hacker News says

1. JtsummersJul 2026
   It mostly just takes practice. A good way to get into it is with property-based testing. It's less formal, but you end up expressing many of the same things (you're at least expressing the post-conditions, if not the rest of the things needed for a proof). With practice, you'll start to understand your systems better, and things like what I wrote up will come to you more easily when analyzing and designing them.

   To move towards formal proofs of code, I like Leino's Program Proofs (uses Dafny), one of the more approachable tutorials on the subject.

   Show morethread
2. JtsummersJun 2025
   https://news.ycombinator.com/item?id=38691437 - Dec 2023, 1 comment

   This only had the one previous submission but I found it interesting. The mentioned book, Program Proofs, is worth checking out if the topic and language interests you.

   thread
3. JtsummersJun 2025
   I agree, using tools more in line with your language is better but I believe the knowledge from learning Dafny ought to transfer well to other systems. And Dafny seems better as a pedagogical system than what I've seen and used for other languages.

   I'm exploring it now as a way to ease colleagues into SPARK. A lot of the material appears to transfer over and the book Program Proofs seems better to me than what I found for SPARK. I probably wouldn't have colleagues work through the book themselves so much as run a series of tutorials. We've done this often in the past when trying to bring everyone up to speed on some new skillset or tooling, if someone already knows it (or has the initiative to learn ahead of time) then they run tutorial sessions every week or so for the team.

   Show morethread
4. mcguireMay 2023
   For some reason, I ended up calling those "axiomatic semantics"; predicate transformer semantics is a much better name.

   One of the weaknesses of PTS for common languages is that statements and expressions have very complicated semantics, compared to the relatively simple semantics of GCL and other simple treatments. One of the nice things about Frama-C (and I think the GNAT SPARK tools) is that, when you are using the WP (Weakest Precondition) module to prove properties of C code, it can automatically generate assertions that describe overflow/underflow, which then forces you to put the appropriate preconditions on function parameters. :-)

   By the way, have you run across K. Rustan M. Leino's recent book, Program Proofs, and the Dafny language. It's the most recent and so far, best book I've seen on the style and technology.

   Show morethread