Re: [mizar] Good news from a mathematician

[Josef Urban <urban@ktilinux.ms.mff.cuni.cz>]

Hi Freek,

> If I understand this correctly you have four options:
> 
> - Do nothing
> - Have something called "requirements"
> - Add a programming language for proof generation to Mizar
>   (and present it like it's a generalization of schemes)
> - Add a way to call external proof generators to Mizar
> 
> Option three is your real proposal, I guess?  

Yes, though the schemes are only used as an example that already now, not 
everything in Mizar has to be proved by the standard checker.  
Later, I was trying to make the idea more digestable by pointing out to 
the strength of the type/cluster mechanism in Mizar.

I do not exclude option four, actually most of my work is probably spent 
on that, but I think that e.g. writing Perl scripts just to generate Mizar 
proof that (1,2,3) * (3,2,1) = 10 is pretty awkward way of doing it.

> But it's not really clear to me what such a programming language would
> look like.

Neither to me, but I think that Mizar should seriously look at other 
systems and try to learn from their approaches.
One feature that I would definitely want is the "kernel" approach, i.e. 
that the algorithm steps can be expanded into the (long) normal Mizar 
proof and can be normally checked and edited. 
E.g. the current implementation of arithmetics in Mizar already does not 
fulfill this.

Best,
Josef