Re: [isabelle] Isabelle Foundation & Certification
On Thu, 17 Sep 2015, Ramana Kumar wrote:
Yesterday, I showed my colleagues that it is possible to prove False in
Isabelle2015 without any warnings or errors and without any use of
axiomatization or oracles.
This is a confusion produced by the paper: example 2 is in opposition to
the axiomatic nature of "typedef" in all published versions of
Isabelle/HOL. See the documentation in the isar-ref manual -- it is
usually up-to-date and authoritative, although sometimes a bit terse.
Of course, one could argue if it is a good idea to treat typedef like
that. This would lead to the very start of a serious discussion -- one
without rumors and unnecessary confusion caused by worrying about
publicity or "bad press".
The trick was, of course, Ondrej's example, but updated to use
"overloading" rather than the deprecated "defs" keyword.
Both are mostly the same. The old "defs" command is declared legacy,
since it complicates critical system interfaces. It is a bit like MS-DOS,
where you still have old CP/M system calls for no good reason, other than
Many of them were surprised, and wanted to know why, when I said that a
patch did exist, it has not been incorporated. I think rumours about
"Isabelle developers" are unavoidable at that point.
In the last 1.5 years, Ondrej has produced various interesting border
cases. I incorporated changes quickly that where valid counter-examples of
expected and documented behaviour -- he also helped in working out missing
The proposed changes of the present paper are genuine feature additions
that go beyond the known and documented model of Isabelle/HOL. This is
why I reduced the priority to a reasonable level. And in fact, we are
talking here about a few months latency of TODO-list pipeline -- things
routinely take much longer than that. Isabelle is not a research
prototype that can be changed arbitrarily at a high rate.
The key question is how users, even power users, can get a more realistic
feeling what the system can do and what not. Maybe we should make a
systematic collection of odd situations, like
https://github.com/clarus/falso for Coq.
Many years ago, system failure happened occasionally in everyday use, so
power users knew what to expect. Actual breakdown is now so rare in real
work that users think the system is unbreakable, and start spreading false
claims to the outside world.
This archive was generated by a fusion of
Pipermail (Mailman edition) and