Re: [isabelle] Need a "What's the foundation of Theory.thy" utility



On 7/9/2013 4:04 AM, Ramana Kumar wrote:
You may be interested in these projects:

https://www.rocq.inria.fr/deducteam/Dedukti/index.html
http://www.gilith.com/research/opentheory/
http://proof-technologies.com/holzero/

The basic idea is to do your proof development in a heavyweight like
Isabelle, and when you're happy with it and want to give it an
extra-special tick, you export a proof and trust it with a tiny,
well-understood checker.

Ramana,

So it seems that, in the future, third-party verification will be a big part of verifying the verifiers.

There's one big problem, which occurred to me lately. I'm getting totally locked into Isabelle due to type classes and Isabelle's nifty type coercion commands. Using those features prevents the possibility of doing an easy translation to any other member of the HOL family. I probably would never have the time to port over what I'm doing, but if I can do something, then I sometimes entertain the idea of doing that something, so timewise, the limitation ends up being a good thing.

With Open Theory, the last time I was looking at it, I think I saw that it doesn't allow new axioms. That's good for third-party verification, but bad if I need new axioms, which I do. With Dedkti, I assume that the problem of either of or both of type classes and no new axioms rules it out. For these, if the foundation is fixed, then it solves the problem of what I'm talking about.

HOL Zero would fall under the "more complex" part of verifying the verifiers. But even HOL Zero would need a utility to report back what the foundation is. If it would be as simple as listing the axiom commands, then it would do that. The idea is for some official utility to authoritatively tell us exactly what axiomatic foundation is being used, other than an exploit, rather than us grepping on some files and us still saying, "I wonder if this is all there is to the axiomatic foundation?" I'll say more about this in reply to Mark's email.

Thanks for the links.

Regards,
GB


N.B. Isabelle cannot yet export to these, as far as I'm aware, but Brian
Huffman wrote some code for importing from OpenTheory.


On Tue, Jul 9, 2013 at 8:40 AM, Gottfried Barrow
<gottfried.barrow at gmx.com>wrote:

Hi,

I don't need this now, but in a year or two, I'd like to have a Isabelle
utility that I run on a theory which tells me what the "foundation" is, and
that also can take a Thy1.thy as the base "foundation", and given Thy2.thy,
the utility reports what additional "foundation" Thy2.thy adds to Thy1.thy.

The foundation would be anything in a theory which would be axiomatic in
nature, and maybe some kind of checksum on things.

Different people are motivated by Isabelle for different reasons. A big
part of my interest in Isabelle is that it's a tool which, at the very
least, replaces the function of peer reviewed journals, to the extent that
it can. That means, at the very least, it's a huge preliminary vetting of
logic in Theory.thy that announces to anyone interested, "The logic in
Theory.thy has been vetted by Isabelle as being correct. It most likely
will not be a waste of anyone's time to wade through 20,000 lines of source
in Theory.thy to figure out what it is, and to find out if it really is
correct."

On a personal level, by all appearances, Isabelle can take the place of
peer reviewed journals, to the extent that it can give you confidence that
you're not producing a bunch of logical nonsense. What Isabelle doesn't do
is solve the "person X is trustworthy and competent" problem on a community
level.

I could dig through the mailing list archives and find where Larry has
said something like, "You have to use Isabelle intelligently." And a while
back, on the HOL4 list, there was a discussion about the possibilities of
people getting proof assistants to do something wrong for either devious
reasons or non-devious reasons. And most recently, on this very list, Falso
was presented as a great logical break through, where, no doubt, still
today, many verifiers, formalizers, and sourcers, not to be confused with
sorcerers, are now full of themselves, mistaking their own logical prowess
with the success that always comes with Falso.

https://lists.cam.ac.uk/**mailman/htdig/cl-isabelle-**
users/2013-March/msg00165.html<https://lists.cam.ac.uk/mailman/htdig/cl-isabelle-users/2013-March/msg00165.html>

Anyway, a "what's the foundation" utility would allow people to do a 10
second check on a theory as a first step, to make sure nothing obvious is
wrong, and to increase the trust factor, and even good people mess up bad
some times.

I assume that there are much more complex problems involved in proof
assistants being completely secure from being hacked, or messed up
unintentionally, but I think it would be good for a person to get a basic
rubber stamp from an official utility that generates a basic report on what
the foundation of a theory is, and that can compare the foundation of two
theories.

No one needs to respond to this. I'm putting it out so maybe in a year or
two there's an Isabelle foundation report utility.

Regards
GB








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