*To*: <isabelle-users at cl.cam.ac.uk>*Subject*: Re: [isabelle] Need a "What's the foundation of Theory.thy" utility*From*: "Mark" <mark at proof-technologies.com>*Date*: Tue, 09 Jul 2013 22:33:13 +0100*Reply-to*: "Mark" <mark at proof-technologies.com>

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.

**Follow-Ups**:**Re: [isabelle] Need a "What's the foundation of Theory.thy" utility***From:*Gottfried Barrow

- Previous by Date: Re: [isabelle] Need a "What's the foundation of Theory.thy" utility
- Next by Date: Re: [isabelle] Need a "What's the foundation of Theory.thy" utility
- Previous by Thread: Re: [isabelle] Need a "What's the foundation of Theory.thy" utility
- Next by Thread: Re: [isabelle] Need a "What's the foundation of Theory.thy" utility
- Cl-isabelle-users July 2013 archives indexes sorted by: [ thread ] [ subject ] [ author ] [ date ]
- Cl-isabelle-users list archive Table of Contents
- More information about the Cl-isabelle-users mailing list