Re: [isabelle] Need a "What's the foundation of Theory.thy" utility
In HOL4, every theorem (a value of type thm in ML), can be inspected to see
the axioms used in its production.
Moreover, all the theorems about any constant (such as might appear in the
conclusion of a theorem) can be retrieved, to help gain confidence in how
the constant was defined. (For example, you could easily check that all the
constants in some theorem were defined in standard HOL4 libraries.)
I'd be surprised if analogous facilities didn't exist in Isabelle already..
On Tue, Jul 9, 2013 at 3:10 PM, Gottfried Barrow
<gottfried.barrow at gmx.com>wrote:
> On 7/9/2013 5:13 AM, "Mark" wrote:
>> Hi Gottfried,
>> 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.
> Also, are
>> 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
>>> to Thy1.thy.
>>> 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.
This archive was generated by a fusion of
Pipermail (Mailman edition) and