Gerwin's Style Guide for Isabelle/HOL. Part 2: Good Style.
The dos and don’ts of Isabelle proofs - Part 2: Good Style. Advanced material for nicer proofs.
With examples and rationale.
Gerwin's Style Guide for Isabelle/HOL. Part 1: Good Proofs.
The dos and don’ts of Isabelle proofs: guidelines for making your proofs more readable, maintainable and enjoyable.
With examples and rationale.
So you want to be a proof engineer?
I want to verify software!
Will prove theorems for money!
What do I need to learn?
You’re a programmer, maybe with a computer science or math degree. You’re interested in program verification and proofs, but have no previous experience in these. You want to learn. Here’s what you should read.
Isabelle Syntax Highlighting in Markdown and HTML
Wouldn’t it be nice to just include snippets of Isabelle code in markdown or html and have them show up rendered with symbols and highlighting?
For instance on a blog? Or a list like the Top 100 theorems? Or on github?
Set your quick_and_dirty flags and read on.
About
The craft, art, and science of interactive machine-checked proof.
This is a blog about formal software verification in general and a tendency towards interactive theorem proving and the prover Isabelle/HOL in particular.
Interactive theorem proving means constructing mathematical proofs where the computer assists in finding the proof and at the same time checks it for correctness. Proof is exciting for software verification, because you can use it as strong evidence for code correctness and for gaining high assurance in security and safety. Interactive proof is one of the most successful methods so far in applying these techniques to real software. It has the potential to fundamentally change how we build and trust critical software.
Formal proof may sound hard, but it is a skill that can be learned. It's turning from art and science into craft.
Contact
Gerwin Klein is Chief Scientist and co-founder of Proofcraft. He is also a researcher in computer science and formal software verification and teaches at UNSW, Australia, applying formal proofs in real-world operating system verification and programming language semantics.