Re: [isabelle] unhelpful comment in Term.ML
On Wed, 11 Nov 2015, Till Mossakowski wrote:
Am 11.11.2015 um 11:17 schrieb Makarius:
In general, Isabelle sources are understood as follows (in that order):
(1) reading the definition in ML
(2) looking through typical uses in ML
(3) peeking at the informal snippets around the formal text, without
taking them too seriously
Note that good software engineering practices would imply the opposite order.
Yes, this is what people sometimes say. I am following that with some
interest over 20 years, which some amusement about the fundamental
divergence of theory and practice.
Systems like Isabelle of approx. 30 years of history define their own
single-element category in this game. It would be interesting to look
closely how it was all done, to learn systematically both from the
successes and mistakes.
Apart from the Isabelle sources, I am routinely exposed to the JVM
sources, which are younger and less advanced in many respects. Despite
the relative success of the JVM platform, I see it as a counterexample in
A positive example is probably the Glasgow Haskell Compiler, see also
http://www.aosabook.org/en/ghc.html -- although I have never looked at the
This archive was generated by a fusion of
Pipermail (Mailman edition) and