Re: PVS GPLed

On Wed, 17 Sep 2008, Freek Wiedijk wrote:

>> to shadow the "ML type thm" in the rest of code,
>
> Sorry, I maybe don't really understand what you mean by
> "shadowing" here.

I meant some kind of overloading - as a Mizar user, you probably know how 
bad these things sometimes can get :-).

> You can define another type "thm" and hope the user will miss
> this attempt at cheating.

Overloading is used for many reasons, it does not have to be intentional 
cheating. Sometimes you get valid overloading just as a result of typo.

> But again, that's not something
> that will happen by accident.  It will not be a bug, but
> a conscious cheat.

With good coding practices or sufficiently simple system.

I think I should repeat that I really like the idea of "small kernel", and 
think that it is really useful for verification. I am probably just trying 
to be a bit skeptical when I hear that something is "safe by design" :-).

Josef