4 ms·
I you prefer readable proofs, try Isabelle or Lean.
by qznc 9y ago
I you prefer readable proofs, try Isabelle or Lean.
- pron 9y agoOr TLA+.
- mcguire 9y agoLamport's structured proofs... should be easier. But I haven't had enough experience to say.
- Zimm_i48 9y agoYou can certainly do readable proofs in Coq the way you would do them in Isabelle, but this requires stating intermediate states explicitly (with assert e.g.) and Coq users rarely do that (mainly because readability is not their goal, I guess).