11 ms·
If you're a programmer that's not tried theorem proving before, I highly recommend giving it a go. It gave me the same 'thrill' I got when I first started progr
by yaseer 9y ago
If you're a programmer that's not tried theorem proving before, I highly recommend giving it a go. It gave me the same 'thrill' I got when I first started programming as a 14-year old and realised a new way of thinking. I find it sharpens your mind in a new, and different way - that's really an exciting feeling.
I prefer Isabelle myself, as I find its proofs more readable in a traditional mathematical sense. Coq however, is probably easier for most programmers to experiment with.
- curryhoward 9y ago> I prefer Isabelle myself, as I find its proofs more readable in a traditional mathematical sense. Just curious, what makes Isabelle easier to read? I haven't tried it.
- yaseer 9y agoIsabelle comes with a proof language layer Isar, designed specifically for readability: https://isabelle.in.tum.de/Isar/ https://isabelle.in.tum.de/Isar/ The structure of Isar proofs then more closely resemble a traditional mathematical proof, with a formalisation close to natural language. You can see the example from Wikipedia: https://en.wikipedia.org/wiki/Isabelle_(proof_assistant) https://en.wikipedia.org/wiki/Isabelle_(proof_assistant) As you can see, the overall structure of the proof is clearer, and you have less dependency of seeing the proof state to understand the proof. The downside to Isabelle is that it introduces a dual syntax, with certain sections written in quotes. There's more to learn syntax and concept wise, but I think it's worth the extra effort for a clearer proof. EDIT: Linked to Wikipedia page for formatting.