On 7/9/2013 5:13 AM, "Mark" wrote:
So you are advocating a utility that would reveal the "foundation" in a
theory. Do you envisage that this utility would have a human aspect to
usage, reviewing that the reported foundation is good, e.g. that the "+"
operator really is the intended "+" operator, etc? By saying a "10 second
check", it suggests not, although maybe I'm missing your point.
No, it's only to list anything that's being used in the theory and
language that's either axiomatic, or might be axiomatic. Also, it would do
some easy checks to rule out the possibility of a person doing sneaky
things, like doing checksum comparisons on third-party files a person is
distributing with their theory, where the local third-party files would be
obtained from the original source.
If someone writes 100,000 lines of source and at the end claims to prove
the Riemann Conjecture, the first thing you want to know is what's in their
THY that's axiomatic, or can't be determined to be axiomatic. The utility
is to give you that information fast.
If someone's not using anything axiomatic beyond what Complex_Main gives
them in Isabelle, then their doing stupid stuff like trying to fool people
with deceptive notation still wouldn't allow them to prove something
that's not true. It would just appear to be something different on the
surface. The statement of a theorem after 50,000 lines of source is always
going to take some effort to figure out what it proves. The utility is to
let you know what the limitations there are to the foundation.
you suggesting that the utility would do some form of automated check on
foundation of a theory, or would it just report what the foundation is?
No, it would just tell me what the axiomatic foundation is for a
particular THY, or what can't be determined in a THY to be axiomatic.
Some things can't be hacked easily. Most people use distribution sources
they've gotten from the official web sites, so you can't hack the
distribution sources and fool anyone but people using local sources. I do
want the utility to tell me what foundation Complex_Main gives me, but I'd
think it's mostly about the utility reporting what people have done to
extend Complex_Main, or done to modify third-party files that aren't part
of the official distribution sources.
The simple part would be listing the axioms used. You might think all I
need to do is grep on "axiomatization", but in Isar, there are more than
"axiomatization". The latest axiomatic command in Isar I've learned about
is "arities". It's not obvious at all it's an axiomatic command.
Right now I'm speculating that when ML is used in Isar, it can't be
determined that the ML does something axiomatic unless you inspect the ML,
but I wouldn't know, which is the purpose of the utility, to get an
official report on what the foundation is.
The purpose is to make it fast, easy, and official what axiomatic
foundation is being used in a THY. For the case where we're not interested
in any logic proved other than what can be proved by importing
Complex_Main, the first thing we would do is run the utility on a THY to
see if that's the case.
I was vague on the details because it's the Isabelle foundation people who
know what possibly can be done axiomatically, but I came up with a scenario:
1) Person 3 releases Theory3.thy. It's distributed with Theory1.thy and
Theory2.thy, which have been released by Persons 1 and 2.
2) I download Person 3's theory, and I run the Isabelle foundation utility
on it. It does a checksum comparison on Theory1.thy and Theory2.thy with
the original files which I obtained. It tells me everything that's in
Theory3.thy that's axiomatic, or can't be determined to be axiomatic.
Additionally, it tells me what's axiomatic beyond what's axiomatic in
Theory1.thy and Theory2.thy
Now, having obtained all that information in a couple of minutes, I can
make an informed decision about whether I want to look at Theory1.thy. If
I'm a professor, and Person 3 wasn't supposed to add anything axiomatic,
and they did, they get bad grade. If I'm an employer, and Person 3 wasn't
supposed to use anything axiomatic, and they did, they get fired.
Some of that I could do myself, but then it's not official, and I don't
know all the details about what can be axiomatic in Isabelle, or what can't
be determined to be axiomatic.
It's not just about checking others, I want the ability to say to people,
"Here's an official report on the foundation I'm using, so you can know up
front what logic my theory is based on."
Like I said to Ramana, even a third-party verifier like yours needs to be
able to give a basic report on what foundation is being used. If all I'm
interested in is standard HOL, then I want to know as fast as possible
whether someone's using standard HOL.
on 9/7/13 8:41 AM, Gottfried Barrow<gottfried.barrow at gmx.**com<gottfried.barrow at gmx.com>>
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.