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



OpenTheory does allow new axioms. (OpenTheory only checks that some
conclusions follow from some axioms; you're free in the choice of
conclusions and axioms, as long as you provide the proof.)

Dedukti should work both for new axioms and for type classes. It does an
encoding into a rich type theory that should support most logical
features... (I'm not so sure about the details).


On Tue, Jul 9, 2013 at 1:47 PM, Gottfried Barrow
<gottfried.barrow at gmx.com>wrote:

> On 7/9/2013 4:04 AM, Ramana Kumar wrote:
>
>> You may be interested in these projects:
>>
>> https://www.rocq.inria.fr/**deducteam/Dedukti/index.html<https://www.rocq.inria.fr/deducteam/Dedukti/index.html>
>> http://www.gilith.com/**research/opentheory/<http://www.gilith.com/research/opentheory/>
>> http://proof-technologies.com/**holzero/<http://proof-technologies.com/holzero/>
>>
>> The basic idea is to do your proof development in a heavyweight like
>> Isabelle, and when you're happy with it and want to give it an
>> extra-special tick, you export a proof and trust it with a tiny,
>> well-understood checker.
>>
>
> Ramana,
>
> So it seems that, in the future, third-party verification will be a big
> part of verifying the verifiers.
>
> There's one big problem, which occurred to me lately. I'm getting totally
> locked into Isabelle due to type classes and Isabelle's nifty type coercion
> commands. Using those features prevents the possibility of doing an easy
> translation to any other member of the HOL family. I probably would never
> have the time to port over what I'm doing, but if I can do something, then
> I sometimes entertain the idea of doing that something, so timewise, the
> limitation ends up being a good thing.
>
> With Open Theory, the last time I was looking at it, I think I saw that it
> doesn't allow new axioms. That's good for third-party verification, but bad
> if I need new axioms, which I do. With Dedkti, I assume that the problem of
> either of or both of type classes and no new axioms rules it out. For
> these, if the foundation is fixed, then it solves the problem of what I'm
> talking about.
>
> HOL Zero would fall under the "more complex" part of verifying the
> verifiers. But even HOL Zero would need a utility to report back what the
> foundation is. If it would be as simple as listing the axiom commands, then
> it would do that. The idea is for some official utility to authoritatively
> tell us exactly what axiomatic foundation is being used, other than an
> exploit, rather than us grepping on some files and us still saying, "I
> wonder if this is all there is to the axiomatic foundation?" I'll say more
> about this in reply to Mark's email.
>
> Thanks for the links.
>
> Regards,
> GB
>
>
>> N.B. Isabelle cannot yet export to these, as far as I'm aware, but Brian
>> Huffman wrote some code for importing from OpenTheory.
>>
>>
>> On Tue, Jul 9, 2013 at 8:40 AM, Gottfried Barrow
>> <gottfried.barrow at gmx.com>**wrote:
>>
>>  Hi,
>>>
>>> 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.
>>>
>>> https://lists.cam.ac.uk/****mailman/htdig/cl-isabelle-**<https://lists.cam.ac.uk/**mailman/htdig/cl-isabelle-**>
>>> users/2013-March/msg00165.**html<https://lists.cam.ac.uk/**
>>> mailman/htdig/cl-isabelle-**users/2013-March/msg00165.html<https://lists.cam.ac.uk/mailman/htdig/cl-isabelle-users/2013-March/msg00165.html>
>>> **>
>>>
>>>
>>> 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.
>>>
>>> Regards
>>> GB
>>>
>>>
>>>
>>>
>



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