Re: [mizar] PVS GPLed

[Freek Wiedijk <freek@cs.ru.nl>]

Makarius:

>Abstract types are fine if you really stay within ML world,
>and have a waterproof implementation of the ML
>compiler/runtime.  I have been told that OCaml is not fully
>type-safe in that respect due to "object magic" features.

Also strings in ocaml are mutable.  It's quite easy to prove
falsity in HOL Light by "cheating" using that "feature".
However, that kind of thing (using Obj.magic or writing into
strings) will _never_ happen without someone making a very
explicit and conscious effort to cheat.  That's not the kind
of thing I'm worried about as a user of a proof assistant.

I think Josef was talking about someone _misunderstanding_
how the system was meant to be used/programmed, and making
mistakes because of that.  But that won't happen.

Of course if your ML is broken, or your OS is broken,
or your processor is broken, still anything can happen,
even without a conscious attempt at cheating.  But that's
not something I would be significantly worried about either.

Freek