Re: [mizar] the Why project

[Andrzej Trybulec <trybulec@math.uwb.edu.pl>]

Dear Freek,

Actually, I thougth (hoped) that maybe it is you who did the Mizar stuff 
in Why :-). There is a lot of the traffic on Mizar Forum related to Why,
so I have nothing to add.
Only, we almost decided that Why be used in the course on program 
verification. We have at leat one year to find out if it fits our 
puposes and, if necessary, to coorect our decision.

All the best,
Andrzej


Freek Wiedijk wrote:
> Dear Andrzej,
>
>
> > Who is interested in the Why project, and who did the Mizar
> > stuff for Why?
>
>
> I am very much interested in Why, although I never really did
> something with it.
>
> The Mizar output was added by Jean-Christophe after he had
> told me that it was not much work to add output for another
> prover.  I don't remember the details, but I think there was a
> little article that was needed to support the Mizar code that
> was generated by Why.  If so, it is probably part of the Why
> distribution.  Jean-Christophe wanted to install that article
> into the MML directory when installing Why.  I told him that
> that was not the proper thing to do, but we never submitted
> this (tiny) article to MML either.
>
> So it would be interesting to know whether the Mizar output
> from Why still works with the current version of Mizar.  I
> doubt it, really.
>
> Freek