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



Hi Gottfried,

I think you're advocating the "proof auditing" idea that I've been trying to
push in recent years.

>> 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)?

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.

> 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?

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

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

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

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

Or if Person 3 is a third party supplier of proofs, trying to cut corners on
their work in an attempt to raise profit margins, they get sued.  This
becomes an incredibly important issue if theorem proving ever makes it
really big.  Unfortunately in this modern world we can't just rely on
"professional integrity".

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

Mark.




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