Re: [isabelle] Parallel proofs issue, potentially in subst method (also, backtraces)



On Mon, 17 Sep 2012, Lukas Bulwahn wrote:

Just to clarify my intentions in this example of a feature request here: Certain features, as the one mentioned above, can be implemented perfectly in Isabelle's "user space". For the implementing developer, many functions then appear to be important for a decent library and we would like to add them to "kernel" modules to make our contribution more visible. However, Isabelle's slogan "fight features" (p.3 of the Isabelle implementation manual) just as the often cited LCF approach forbid to modify and extend kernel modules, just because of a temporal state of mind. Coincidently, Makarius is the person, who enforces these matters in our system and repository---Hence, the statement "We can't get it past Makarius", really means we do not have any substantial reason to modify the kernel.

First of all, a citation is just a citation, not a literal statement. The ones on the front-part of the Isabelle/Isar manual do have some correlation with the received Isabelle development process and its challenges, which is why I've put them there, but eveybody needs to start his own thinking process to see behind the surface and the actual things
in the background.

I've recently come across a very interesting lecture by Alan Kay on "Programming and Scaling" http://tele-task.de/archive/video/flash/14029/ which might lead to more citations from him ending up in that spot of the implementation manual. I particularly like one of his explanations (probably from another talk) about the fundamental importance of architecture: instead of turning many bricks naively into an amorphic pile of bricks, to make a sophisticated building you need to follow certain structuring principles that you need to learn first. And the main focus of that talk is then about learning and education, especially in the US, especially science and math education.

Alan Kay is an interesting person in many respects. He has now grown old and wise, and can go beyond the follies from his youth, most notably the "object-oriented" movement that he started. (He is the inventor of the term "OO", so its fun to see him bashing that a lot now.)


	Makarius






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