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



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 its
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.  Also, are
you suggesting that the utility would do some form of automated check on the
foundation of a theory, or would it just report what the foundation is?

Mark.

on 9/7/13 8:41 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
>
> 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.