Re: [isabelle] Length of Proofs
I take your first point, that "everything is accessible from ML", but
in a practical sense, I would say it's not because the code is so
difficult to understand. (Much more difficult than either Isabelle as
it was in 1997, or HOL, to give examples within my experience.)
In a way, my first contribution to this thread was to make it clear that
both "development" and "ordinary reasoning" are intertwined - there was
quite a lot of "development" involved in getting the right combination
of compound tactics and proof steps to avoid a proof script which would
have been 10000 lines long.
The bigger issue is that pen and paper proofs I do and publish in a
journal will be available as long as people want to read them. The
Isabelle proofs I do are in Isabelle 2005, and include theory and ML
files from 1997, and so will in the future be inaccessible to anyone who
doesn't (or can't) install Isabelle 2005 (which only seems to work with
one particular version of PolyML). Given the philosophy of Isabelle
developers, prospective users need to be warned that if they want to
write proofs which will be accessible to future researchers, they need
to be done in print.
Finally, it's worth pointing out that no one in this thread has actually
come up with a suggestion about how to do the sort of proof which was
the subject of my original post other than using Standard ML (which, I
understand, was designed for exactly that purpose).
Lawrence Paulson wrote:
As I see it, there are advantages to both interfaces. And everything is accessible from ML simply because it is the implementation language, although of course this access may not be very convenient. I think it's generally accepted these days that the ML level really is more appropriate for development than for ordinary reasoning. It isn't realistic to support both Isar and the ML level as the day-to-day user interface; even with unlimited resources, such duplication wouldn't be very elegant.
Isabelle has undergone very rapid change over the years, and this has meant leaving a lot of old practices behind. I know that it has caused users difficulties in the past, and it's unfortunate, but maintaining upwards compatibility is also very difficult. As one of the earliest Isabelle users, you naturally feel this much more than others do.
On 17 Nov 2012, at 06:04, Jeremy Dawson <jeremy at rsise.anu.edu.au> wrote:
My understanding has been that you - or someone - introduced new features in Isabelle which were accessible only from Isar, not from the Standard ML interface.
In my book this discourages the use of Standard ML, and also provides an explanation for it having "come out of use", regardless of its relative merits as a user interface language.
This archive was generated by a fusion of
Pipermail (Mailman edition) and