Re: [isabelle] Isabelle Foundation & Certification





On 20/09/2015 16:02, Makarius wrote:
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

I'm afraid that most of the people who have spoken up have looked at the issue in the light of example 2 and have already decided that this is a no-brainer. Their contributions were based on that conclusion. And in some cases also on Ondrej's experiments that showed that neither the distribution nor the AFP contains any such circularity, neither intentional nor accidental. Hence we have not heard any views asking for such circularities to be accepted. But maybe you want to convince us otherwise.

Tobias

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


     Makarius


Attachment: smime.p7s
Description: S/MIME Cryptographic Signature



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