News for hackers. Stuff that matters.
Re:My unusual hobby by Zimm_i48 on Monday November 27, 2017 @07:40AM (#15786850)
You 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).

There are no comments on this comment yet.