Re: [isabelle] Need a "What's the foundation of Theory.thy" utility
You asked me a specific question at the end your email, so I put it here
first, so it doesn't get lost in my noise below.
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.
Can you spell out in what sense HOL Zero does not meet your aims on this?
I'm eager to hear about any ideas for improving it.
I think it's merely that you don't support Isabelle/HOL. I have no
loyalties when it comes to proof assistants. I'd abandon Isabelle
tomorrow if I found better software. But I'm not going to find anything
else. For natural deduction based logic, there's nothing out there that
comes close to providing the features that Isabelle provides, and it
gets better with every release.
If you tell me, "But I do support Isabelle/HOL. You can run HOL Zero on
any Isabelle/HOL theory that does anything that Isar allows you to do."
I say, "You do? Man, item number n of large integer M of things I've
wanted that someone has already implemented, but I didn't know about.
Here I've been asking for some basic utility when I can already run HOL
Zero on my THY to verify the verifier, to check the checker, to go the
extra mile to get an automated rubber stamp of what I'm doing in logic,
logic being a tricky deal, full of potential pitfalls, with people
needing to have some preliminary confidence in what I've done before
they're willing to figure out what I've done."
On 7/9/2013 4:33 PM, "Mark" wrote:
I think you're advocating the "proof auditing" idea that I've been trying to
push in recent years.
No, I'm a just a user, and I'm not remotely qualified to be involved in
the debate over what it takes to "verify the verifiers". I want people
like you to be a verifier watchdog, but I'm no more qualified to know
what proof auditing should entail than I am to know what it takes to
find security holes in Java or Windows.
What I'm primarily talking about is what a language can declare; I'm not
concerned with whether the engine that implements the language has
integrity, or can be exploited through security holes. What I'm
requesting is simple. Given two languages, Isabelle/ML and
Isabelle/Isar, and two theories, Theory1.thy and Theory2.thy, report to
me what statements in ML and Isar are made in the theories that are
axiomatic, and anything else that someone decides to label "the
foundation", and tell me what is axiomatic in Theory2.thy that goes
Do you envisage that this utility would have a human aspect to
its usage, reviewing that the reported foundation is good ....
No, it's only to list anything that's being used in the theory and
language that's either axiomatic, or might be axiomatic.
By "axiomatic" are you referring to any HOL axioms, constant definitions,
type definitions, etc (i.e. what I call "assertions", which is what
mathematicians call "axioms") made in the theory, or are you referring to
just HOL axioms (i.e. the completely unrestricted form of HOL assertion)?
This is where I'm not the one who's supposed to be deciding on
everything in Isabelle/HOL, Isabelle/Isar, Isabelle/ML, and
Isabelle/Pure that deserves to be labeled "axiomatic".
I never made any real progress in HOL4, but it appears that what is
axiomatic in HOL4 is more straightforward and obvious than what's
axiomatic in Isabelle/ML, Isabelle/Pure, and Isabelle/Isar.
At the easiest level, it's keywords in Isar that are axiomatic, two of
those keywords being "arities" and "axiomatization".
I'm under the impression that Isar constants aren't axiomatic, that they
don't allow you to prove anything other than they exist, or that they
always return a value because HOL functions are total. There is the
undefined constant in HOL.thy "axiomatization undefined :: 'a", line
195, which Lars pointed out, so it looks like constants alone don't give
us anything axiomatic.
As far as types, there is this statement in isar-ref.pdf:
If you introduce a new type axiomatically, i.e. via typedecl and
axiomatization, the minimum requirement is that it has a non-empty
model, to avoid immediate collapse of the HOL logic.
What does that mean in the context of what in Theory.thy is the
foundation? I don't know completely, but I do know that I used
"typedecl" and left the HOL function "eq" undefined for my new type, and
after I stated an axiom, my logic was inconsistent because "eq" wasn't
defined for my new type. So, apparently, typedecl qualifies as being
listed in "the foundation".
To summarize, the utility is supposed to tell me what's axiomatic in a
THY, so I can then tell you what's axiomatic in a THY.
Don't you mean "yes" as the answer to my quesion? Surely whatever
foundation is being printed out by the utility needs to be examined in
detail, with all its subtlety, by a human to make sure it's good foundation
rather than nonsense. This is not a 10 seconds exercise, even with the most
user-friendly utility imaginable.
No, other than the utility reporting that the logic is inconsistent. If
someone puts in an axiom that will give them the Riemann Hypothesis, but
which isn't the Riemann Hypothesis, how is the software supposed to know
that it's nonsense, unless it makes the logic inconsistent?
You could have a black list of bogus axioms, but that's no great
feature. Most likely, if a crackpot published a THY with 10,000 lines of
source claiming to prove the Riemann Hypothesis, there would only be a
few axiomatic statements in it. What's important is that the utility
tells me that on line 4500 "axiomatization" is used, and what the axiom
is. Or maybe "arities" is used in a clever way to get the result, but it
tells me about it, and it's my job to judge whether it's valid.
For most people using Isabelle/HOL, it's not about whether additional
axioms are nonsense or not, it's that Isabelle/HOL shouldn't be extended
axiomatically in any way. The foundation to check any THY against is
Complex_Main.thy, and mostly, people don't want anything axiomatic
The nature of logic is I'm free to start with whatever axioms I want.
The main thing is to clearly know what the foundation is, not to have
someone tell you that it's nonsense. What I'm asking for is a 1 day or a
1 week job. If I ask for more, no one has the time to do it.
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.
I don't get what you're talking about here with checksums. Is this used by
Isabelle or something?
The utility doing a checksum on a file using a known good checksum would
be a secondary feature. This falls under "easy integrity check" rather
than "axiomatic declaration in the language".
The idea is that Trusted Person has released Hol_Extension.thy and it
has become a standard extension of HOL, but it's not part of the
Isabelle2013 distribution, and people are distributing it with their own
theories. I give the utility a MD5 checksum that Hol_Extension.thy is
supposed to match when a checksum is run on the file. If it doesn't
match, then the person is not distributing the right file, and maybe
they edited it.
Okay, but if I have the known good Hol_Extension.thy, then can't I just
copy it over the one distributed? So maybe the purpose is just to try
and bust amateur deceivers who are trying to do easy hacks.
The checksum idea was just part of brainstorming on the concept of some
minimal thing that a utility could do to keep people from wasting our
time with bogus theories.
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.
This really does sound like a tool for supporting proof auditing.
You would have to tell me what proof auditing is, but I don't classify
it as proof auditing. "Proof auditing" implies that proofs need to be
checked because there's the possibility that the underlying software is
being exploited or has bugs.
I use the phrase "or can't be determined to be axiomatic," but I'm only
speculating that a person might need to look at a block of ML to
determine whether it declares something axiomatic. The utility would
report on ML that's used which needs to be inspected by a human, and a
person who knows enough could decisively determine whether the ML is
axiomatic. That's what I was talking about, and just knowing about
anything that's axiomatic.
If I state a axiom that gives me a proof of the Riemann Conjecture,
there's nothing that needs to audited. The proof is correct, given the
axiom. Logically, there's no problem with the proof.
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.
That's right, the proof audit should only examine what's been used.
Intermediate stuff is irrelevant if it doesn't get used. Specifically you
need to be examining all axioms and definitions that get used in the proof
of the supposed theorem.
Well, there's some divergence here between you as a qualified proof
auditor, and me as an end user.
I don't concern myself with checking what's imported with
Complex_Main.thy, though I want to know about foundation it provides. I
have to trust the Isabelle2013 distribution. If the utility reports to
me that the foundation of Theory1.thy is exactly the same as
Complex_Main.thy, except for Axiom1 on line 4015, then all I need to do
is look at Axiom1. In fact, if I'm not interested in any theory that
extends Isabelle/HOL axiomatically, I don't even need to look at Axiom1,
all I need to know is that it's there.
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.
Yes, this is where proof porting comes in. Ideally you want to be able to
port the proof object to a target system (using proof recording), replay the
proof and examine what axioms and definitions are getting used.
HOL Zero is specifically designed for this target system role, of course.
It is more trustworthy than any other system (although some people seem to
disagree..). And it has the 'get_all_axioms', 'get_all_const_definitions',
'get_all_const_specifications' and 'get_all_tyconst_definitions' commands,
primarily to help proof auditing. These reveal what gets used in the ported
proof, because the base HOL Zero system has so little theory itself.
I'm all for you giving me a tool where I can say, "Please, everyone,
here's the screenshot from the HOL Zero tool showing that what I've done
in Isabelle has passed the HOL Zero integrity check. You still have to
figure out what I've proved, but it tells you what my foundation is, and
that the underlying logic hasn't been hacked. I'm working hard here to
show you that my logic is legitimate, without having to beg some
establishment journal to give me access, which they're not going to do,
and I'd rather do it with automation anyway, so I can be as
unprofessional as I want to be."
It's worth repeating, that I'm all for you giving me HOL Zero to verify
Isabelle/HOL, and lots of other people would want that too. But it seems
at this point, that's years away from happening. They'd have to hire
you, and you'd have to go to Germany or England to get it done any time
This archive was generated by a fusion of
Pipermail (Mailman edition) and