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 old customs.

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 details.

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 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 MHonArc.