[isabelle-dev] purpose of isabelle-dev

[Makarius]

On Sun, 28 Oct 2012, Tobias Nipkow wrote:

> There are practically no such ML questions unrelated to theorem proving 
> on isabelle-users. Because 90% of the subscribers do not want and need 
> to know about it (thanks to Isar). The remaining 10% also subscribe to 
> isabelle-dev. But since the number of such questions is very small, it 
> is not worth arguing about it.

Before this confusion from 10 years ago (Isar = users, ML = developers) 
comes up again, I would like to point to 
http://www.lri.fr/~wenzel/Isabelle_Orleans_2012/slides.pdf

It was presented at the Orleans Isabelle tutorial, after the first hour of 
warming up with the editor.  The quick start was as follows:

   * http://en.wikipedia.org/wiki/File:Blind_monks_examining_an_elephant.jpg
     points to the Asian tale of http://en.wikipedia.org/wiki/Blind_men_and_an_elephant

     This metaphor is actually stemming from Larry: it was his spontaneous
     reaction on the Isabelle overview we've had on TPHOLs2008.  The point
     is that it is hard to give a full picture of the system.  If you hold
     only the tail or tusks of the beast, you still have just some
     partial aspects, and need to avoid the temptation to make an inductive
     closure from that information.

   * Brief history about "family relations" of LCF, HOLs, Isabelle, Coq

   * "Some Isabelle languages" on slide 4; for convenience the material is
     copied here:

   Logic:

     Isabelle/Pure: Logical framework and bootstrap environment
     Isabelle/HOL: Main application logic with many add-on tools

   Programming:

     Isabelle/ML: Implementation and extension language (strict functional
       programming, exceptions, interrupts, parallel evaluation)
     Isabelle/Scala: System programming and connectivity on the JVM

   Proof:

     Isabelle/Isar: language for Intelligible semi-automated reasoning
     Isabelle document preparation: formal text as PDF-LATEX


All of that is user-space, of course.  For example, I briefly showed 
code-generation in the second hour like this:

declare [[ML_trace]]

ML {*
   @{code List.map}
*}

This gave the attendants some impression how things work, without having 
to pretend that the system is just Isabelle/HOL, i.e. another HOL clone.


The easy access to Isabelle/ML within Isabelle/Isar is one of the big 
assets of Isabelle compared to Coq.  If it were not part of the user 
space, I would not have spent all these efforts in the past few years to 
make it easily accessible, with full IDE integration.  (The ML bootstrap 
environment for Isabelle/Pure is different from that.)


We don't need separate mailing lists for each Isabelle language.  We 
desparately need a mailing list that supports the Isabelle development 
process reliably.  On isabelle-dev we still have a lot of drop-outs in 
this respect.


 	Makarius