News for hackers. Stuff that matters.

A comment on My unusual hobby. Parent comment

Re:My unusual hobby by codeflo on Saturday November 25, 2017 @01:04PM (#15777008)
Is that partially a tooling problem, i.e. would it help or even be possible to show those intermediate “proof states” (as used by the grandparent) live in the IDE while you type?
[ Parent | on HN ]
Re:My unusual hobby by mcguire on Saturday November 25, 2017 @01:11PM (#15777055)
Stepping through the proofs in the IDE is the only way to understand them. But that is like stepping through a program in a debugger---it's inefficient if you have a lot to understand.
[ Parent | on HN ]