Some tips on doing program proofs in Creusot
– This is a Work In Progress! Going to add more stuff soon™ –
Creusot
A year ago I had done exactly zero program proofs.
I have now done more than zero program proofs, and have, in my opinion, become pretty good at doing program proofs in Creusot.
I have therefore, with the intention to make the transition from having done zero proofs to being able to prove useful programs in Creusot a little bit less painful, written up some of my learnings. There is probably a bunch of things which I once found hard, and then understood, and now have forgotten that is hard, so feel free to reach out to me or Xavier Denis or open a issue or something if you’re struggling.
This is in no way a complete guide, but I think the current test suite of Creusot combined with these writings, my thesis, and the proofs found in CreuSAT, should make the experience of learning Creusot a lot less shit than it used to be.
Also, Creusot has become a stupid amount better since I started. I now has a lot fewer rough edges, support for more features, and is able to prove things much more easily.