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



Mark,

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:
Hi Gottfried,

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 beyond Theory1.thy.

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 beyond that.

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 soon.

Regards,
GB




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