\documentclass{llncs}
\begin{document}

\title{Wishes for Mizar}
\author{Freek Wiedijk\\\email{freek@cs.kun.nl}}
\institute{University of Nijmegen}
\maketitle

\begin{abstract}
Here is a list of the things I desire for the Mizar system.
\end{abstract}

\setcounter{section}{-1}
\section{}
In an e-mail to Grzegorz Bancerek I mentioned that
there were some things I'd like to see different in Mizar.
He asked for a description.
So here are some things I would like to be different.

These are listed in order of importance (most important first).
The first three wishes are easy, the last two wishes are hard.

\section{Manual}

Mizar has no proper documentation.
This is unacceptable.
Please write something.

It should at least consist of a hundred page reference manual
and a thirty page tutorial.
It should be in English.

Once you do this: keep it up to date.
So if a requirement is added to the language then add it to the manual,
if the type of real numbers becomes \verb|real| \verb|number|
instead of \verb|Real| then modify the tutorial,
etc.

\section{Weird characters}

The `mathematical' characters look nice if you have the right fonts
installed,
but they make everything complicated.
The fonts often are not available, these characters are hard to type,
these characters make the MML web pages ugly because of the
GIFs.

I know these characters are already gradually being phased out.
I'd prefer to see this problem solved in one big substitution operation.

I don't consider going to full Unicode an improvement.
On the contrary.
Please only use ASCII characters with codes between 32 and 126.

\section{Modules}

The \verb|environ| part of a Mizar article is difficult to get right.
I would like to see three changes to the Mizar module system.

\subsection{Vocabulary names versus article names}
Vocabulary names and article names are similar but different.
For instance one vocabulary is called \verb|PFUNC1| but the article
is called \verb|PARTFUN1|.

Make them really the same name space.
So have each vocabulary `belong' to an article.

\subsection{Vocabulary files versus article files}
Vocabulary files are separate from the article files.
It is not very practical to have to have a small `satelite file'
when developing an article.

I'd like to see the two kinds of files merged.
Put the vocabulary files as a `vocabulary section' at the top
of the article file.
Or have `vocabulary definitions' among the other kinds of definition.

\subsection{Separate directives}

There are a several `library directives':
\begin{itemize}
\item \verb|vocabulary|
\item \verb|notation|
\item \verb|constructors|
\item \verb|clusters|
\item \verb|definitions|
\item \verb|theorems|
\item \verb|schemes|
\end{itemize}
In practice the same article name generally occurs in all of them.

I'd like to see this simplified.
Just have one \verb|import| directive which imports all
the features of the article at the same time.

This will make things a bit slower.
This is not important.

\section{Not only Intel}

Mizar only runs on computers with an Intel processor.
I don't own one.
This means I can't run Mizar properly.

Please port Mizar to a language that can be run on most processors.

\section{Partial functors}

The semantics of functors in Mizar treats
typing and predicates differently (\verb|sqrt -1| doesn't satisfy
the defining predicate of \verb|sqrt|, but it {\em has\/} type
\verb|Real|).
This hardwires the axiom of choice
(in fact something stronger: a choice operator)
into the first order logic.

I'd like to have something different from the way it is now.

This probably would make the system harder to use
(you might have to prove being allowed to use a functor before being
able to use it)
but it would make things more elegant mathematically.

\end{document}