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



You may be interested in these projects:

https://www.rocq.inria.fr/deducteam/Dedukti/index.html
http://www.gilith.com/research/opentheory/
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.

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