Re: [isabelle] Proof by analogy and proof stability in Isabelle

I think an important aspect of this topic is the issue of legal liability.  
If you use a theorem prover to prove a theorem, that is used to create a query into a medical ontology,
 which is then used in the diagnostic train for determining a patients treatment protocol you better 
be able to stand up in court and defend it.  I would not want to tell a judge: "at this step we invoke 
the magic word 'auto' which does 'something unknown' and then we went on from there'.

-----Original Message-----
From: cl-isabelle-users-bounces at [mailto:cl-isabelle-users-bounces at] On Behalf Of Makarius
Sent: Friday, April 30, 2010 8:10 AM
To: isabelle-users at
Subject: Re: [isabelle] Proof by analogy and proof stability in Isabelle

On Fri, 30 Apr 2010, Brian Huffman wrote:

> On occasion I have had significant amounts of trouble getting old proof 
> scripts to work again. The process is most difficult with theories that 
> were developed for older versions of Isabelle: Porting a proof directly 
> from Isabelle 2005 to 2009 can be much more difficult than continuously 
> adapting the same proof to a series of development snapshots. I would 
> suspect that most users have to deal with these large version-jumps more 
> often than the developers do.

Jumping over several Isabelle releases at the same time is indeed very 
hard.  Users can avoid that by following the official release schedule -- 
the distances between Isabelle2007 -- Isabelle2008 -- Isabelle2009 -- 
Isabelle2009-1 are not too big.

Isabelle2005 -- Isabelle2007 is in fact a counter example, with 25 months 
between the releases and the result being rather unstable.  At that time 
it was not completely clear if we would ever recover from a continously 
"intermediate" state, and join the fate of notorious projects such as 
SML/NJ or the STIX fonts.

Anyway, one should distinguish between really large libraries and the 
underlying system infrastructure.  A library could well be developed in a 
Wikipedia style, and people in Nijmegen are working on that, for example.


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