Re: [Hol-developers] how many soundness bugs?

[Peter V. H. <pal...@tr...>]

The date of Ray's bug was 1994, I believe.

Peter

On 10/1/07, Peter Vincent Homeier <pal...@tr...> wrote:
> I believe that Ray Toal (http://www.technocage.com/~ray/) a friend of
> mine at UCLA, found the last soundness bug in HOL to be discovered "in
> the wild".  It was a problem I think with INST_TYPE that didn't handle
> free type variables in the hypotheses correctly, and he could pove "1
> = 2" or some such result.
>
> But you should contact Ray for details.
>
> Peter
>
> On 10/1/07, Konrad Slind <sl...@cs...> wrote:
> > Last person who found one was Bruno, based on close
> > reading of src/0/Thm.sml, which he was modifying to
> > support execution primitives in computeLib.
> > Before that, I don't recall one since about hol90 version 4,
> > which was sometime in 90/91, I guess.
> >
> > I think Michael fixed some bugs in the experimental kernel
> > that could have been problematic. Not sure if they were
> > in released code though.
> >
> > Good luck with the grant proposal!
> >
> > Konrad.
> >
> >
> > On Oct 1, 2007, at 5:50 AM, Hasan Amjad wrote:
> >
> > > Would anyone know roughly how many soundness bugs have been discovered
> > > in released versions of HOL in the past decade? I need to extol the
> > > virtues of LCF-style implementations for a grant proposal. TIA.
> > >
> > > Cheers,
> > > Hasan
> > >
> > >
> > > -----------------------------------------------------------------------
> > > --
> > > This SF.net email is sponsored by: Microsoft
> > > Defy all challenges. Microsoft(R) Visual Studio 2005.
> > > http://clk.atdmt.com/MRT/go/vse0120000070mrt/direct/01/
> > > _______________________________________________
> > > Hol-developers mailing list
> > > Hol...@li...
> > > https://lists.sourceforge.net/lists/listinfo/hol-developers
> >
> >
> > -------------------------------------------------------------------------
> > This SF.net email is sponsored by: Microsoft
> > Defy all challenges. Microsoft(R) Visual Studio 2005.
> > http://clk.atdmt.com/MRT/go/vse0120000070mrt/direct/01/
> > _______________________________________________
> > Hol-developers mailing list
> > Hol...@li...
> > https://lists.sourceforge.net/lists/listinfo/hol-developers
> >
>
>
> --
> "In Your majesty ride prosperously
> because of truth, humility, and righteousness;
> and Your right hand shall teach You awesome things." (Psalm 45:4)
>


-- 
"In Your majesty ride prosperously
because of truth, humility, and righteousness;
and Your right hand shall teach You awesome things." (Psalm 45:4)