[Date Prev][Date Next] [Chronological] [Thread] [Top]

Re: [mizar] notes on isabelle vs. mizar


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