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 software engineering.

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 actual sources.


	Makarius





This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.