[mizar] Re: R: PVS GPLed

[Jesse Alama <alama@stanford.edu>]

Freek Wiedijk <freek@cs.ru.nl> writes:

>>By the way, what do you mean by 'old style "from"'?
>
> Nowadays to use a scheme you need to define predicates
> and/or functors that match the arguments of the scheme using
> "defpred" and "deffunc".  Mizar used to be able to figure
> out by itself what the instantiations of the predicates and
> functors in the scheme were just by looking at the shape
> of the formulas.  I liked it that way.
>
> I'm sure that sometimes it was ambiguous, and that the
> implementation of _how_ it worked was a big mess.  But in
> practice it worked well for me, and I miss my proof looking
> clean, without all the "defpred" noise.  When presenting
> Mizar in a talk this is often one of the things that makes
> my examples less convincing.

I'm surprised that this feature would be taken out.  What's the reason
for that?  I hate to ask a rhetorical question, but isn't one of the
goals of the mizar language to be as close as possible to informal
mathematical vernacular?  Shouldn't the direction of development be
toward a richer language and/or more automation?  Some mathematicians
might prefer to express themselves informally in the way that mizar now
enforces ("Let A(x,y,z) be the predicate defined by..."), and those
mathematicians can use defpred or deffunc in their mizar proofs.  But it
would be nice if mizar also supported a less explicit argumentative
style.

Jesse

-- 
Jesse Alama (alama@stanford.edu)