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


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.


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.


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