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'.
From: cl-isabelle-users-bounces at lists.cam.ac.uk [mailto:cl-isabelle-users-bounces at lists.cam.ac.uk] On Behalf Of Makarius
Sent: Friday, April 30, 2010 8:10 AM
To: isabelle-users at cl.cam.ac.uk
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