[isabelle] Need a "What's the foundation of Theory.thy" utility
- To: USR Isabelle Mailinglist <isabelle-users at cl.cam.ac.uk>
- Subject: [isabelle] Need a "What's the foundation of Theory.thy" utility
- From: Gottfried Barrow <gottfried.barrow at gmx.com>
- Date: Tue, 09 Jul 2013 02:40:20 -0500
- User-agent: Mozilla/5.0 (Windows NT 6.1; WOW64; rv:11.0) Gecko/20120312 Thunderbird/11.0
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
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