Once we have a high-level interface to the proof state, Cochon will only be a
trauma that we will collectively try to forget.
Part of the therapy will be to turn it into a stupid debugger, stripping out
the programming feature, turning it into some kind of proof state explorer. The
"idea" being to be able to load a development built by the high-level interface
and navigate in it (to track bugs in the high-level system for instance, or for
pure masochisms).
This means: cleaning up the mess that Cochon currently is. This also means: not
adding more cruft to it.
Original issue reported on code.google.com by pedag...@gmail.com on 11 Aug 2010 at 6:08
Original issue reported on code.google.com by
pedag...@gmail.com
on 11 Aug 2010 at 6:08