Re: [mizar] notes on isabelle vs. mizar

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

Hi Slawomir,

On Tue, 25 Mar 2008, Slawomir Kolodynski wrote:

> I would like to comment on the comparison from the
> point of view of an Isabelle user. I use Isabelle/ZF
> for my formalized mathematics hobby project.
>
> ---+ browsing of Isabelle formalizations sucks
> To me the preferred view of Isabelle theories is the
> proof document in PDF. It is very readable and easy to
> search. It is true that the HTML documents produced my
> Isabelle might use the possibilities of web browsing
> much better. However, parsing Isar is easy enough that
> a motivated person can roll out his/her own rendering
> of the theories. I have done so for my project, see
> http://formalmath.tiddlyspot.com .

Cool! (Just add browsing of symbols and do it for all of Isabelle, and 
it's better than anything existing for formal math today :-)
I was considering jsMath for TeX-printing of the Mizar HTML pages a 
while ago, but it looked too slow in preliminary experiments, perhaps I'll 
reconsider

> ---+ XSymbol vs. ASCII
>     XSymbol-ed texts look nice in Emacs and PDF, but
> not in ASCII;
>
> I don't quite understand why it would be a desirable
> feature for Isabelle theories to look nice in an ASCII
> editor.

because it's quite a strong assumption that everyone will only want to use 
(X)Emacs

> ASCII editors are not good tools for
> presenting or authoring mathematics, formalized or
> not.

I would agree with presenting, authoring is a different matter. The Mizar 
team even went from nonASCII-allowed to ASCII-only couple of years ago for 
purely practical reasons, and people got used very quickly to "in" instead 
of the \epsilon character.

I think that this might change over time, e.g. with good Unicode tools (in 
this sense XSymbol is still ASCII, which is good).

> ProofGeneral is a decent authoring tool for
> Isabelle and PDF proof documents are good for
> browsing.
> One of the features of Isabelle that I like a lot is
> that it supports a (potentially) unlimited number of
> symbols.  This allows to create renderings of
> formalized text that are very close to traditional
> mathematical notation. It is just not possible with
> the set of symbols limited to ASCII.

yes, I think the options are
1) input in a special form, which looks good in some editor
2) input in ASCII, and do the good-looking stuff as an optional 
presentation layer

I generally dislike (1) for any coding, mainly because it limits the tools 
(think grep, sed, awk) that could be used on the code. But this is more 
about formats like Microsft Word than XSymbol.

Josef