|
|
|
|
|
|
by Jtsummers
2 days ago
|
|
|
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. |
|
|
If practice is enough to get a formal system to be correct then why are we doing all this in the first place? Just write correct software! Oh, you can make mistakes? Exaclty! Just like when writing the spec.