Is a wiki the most appropriate system for a professional math repository?
Robin Green
it can be helpful to revisit initial assumptions.
My current thinking on wikis for repositories of formalisations is that
wikis can be great for text (e.g. documentation, encyclopedias,
teaching notes, discussions etc.), but distributed version control
software such as monotone or darcs are best for code. And I view
many types of formalisations that can be checked by a computer program
as, not just "like code", but actual code. For example, in Coq you can
do proof extraction to generate OCaml code from proofs, so it's not too
much of a stretch to regard Coq as a compiler and its input files as
source code, in that scenario.
Many traditional software projects (in C, Java etc.) have certain
standards which maintainers try to uphold, by acting as "gatekeepers"
and rejecting or modifying "bad code" that is submitted. The Linux
kernel is a good example of such a project - and in that project a
submission may be reviewed by *multiple* "gatekeepers" before being
accepted into Linus' official mainline.
Standards for such projects may include some or all of the following:
* The code should compile
* The code should continue to compile in future, by using proper
configuration management (this idea is actually usually not required
or not enforced stringently enough in open source projects)
* Obvious bugs should be eliminated
* Duplicate functionality should not be introduced
* The code should not simply ignore error conditions
* Complicated or lengthy code should not be used where shorter or
easier-to-understand code would meet the project's goals and standards
just as well
* Copyright and authorship data should be given in each file
* The code should be relevant to the project
All of these criteria - or close analogs thereof - could be relevant to
a formalisation project.
Some people who are new to formal methods may be under the impression
that if a proof is computer checked, and the software that checks it
is working, then there can be no problem with the theorem or the proof.
This, of course, is false. The proof might be unnecessarily long. The
theorem you have proven might be mis-stated, so that you are actually
proving something trivial when you thought you were proving something
profound. If you are extracting code from the proof, a different proof
might be more suitable for that purpose because it might yield more
efficient code. You might be depending on a volatile theorem library
that will change in an incompatible way in the future.
Of course, you can allow anyone to edit wiki pages and then act as a
gatekeeper by editing or reverting changes you don't like. That's one
possible approach. However, by using a wiki and advertising that "anyone
can edit" you are:
* attracting vandals and spammers - a problem which
properly-secured source code repositories do not have, to my knowledge
* creating a presumption in many people's minds in favour of earlier
changes, so that it can be seen as "rude", "alienating" and
"contentious" to revert earlier changes if they do not 100%
objectively fail to meet the project's standards (and sometimes even if
they do!). By contrast, in a gatekeeper-mediated software project at
least some of the "burden of proof" (no pun intended) falls on the
submitter to justify why their change should be accepted into the
project. (This of course varies somewhat from project to project.) I
think this difference is more to do with standards of etiquette and
human psychology than anything else.
* encouraging people to use an interface - a wiki - which isn't, at
present, anywhere well enough integrated into a theorem prover (or other
formalisation tool). If I were to use a standard wiki interface to edit
my Coq developments, I'd have to keep pressing Preview after entering
each line to see what I was doing - resulting in a re-checking of the
entire file - not very efficient. Or I'd have to work on my own
installation of CoqIDE, and copy-paste my files into the wiki when I
wanted to commit my changes, which would be annoying, and would not
provide as good merge support as distributed version control software
provides.
Moreover, there are efficiency and political arguments against relying
on the cloud:
Efficiency: Theorem provers can be quite resource-intensive - at
present, it might make more sense to force users to run them locally.
After all, they'll likely get faster feedback that way - which is very
important for the complicated proof developments I work on.
Political: Those who support the Free Software Movement, like me,
believe that it is a bad habit to rely on cloud computing
infrastructure (that you don't administer yourself), because you
don't have the freedom to inspect what's running nor to change it. (Of
course, it's hard to be a purist about this - I use GMail.)
I don't buy the "it needs to be dead simple to use" argument, because,
let's face it, theorem provers are *not* dead simple to use. You need to
learn a language and that takes time. If you've got time for that,
you've got time to install an .exe file, or pick e.g. Coq to install
from your operating system's package management application, or
whatever.
--
Robin
Slawomir Kolodynski
> My current thinking on wikis for repositories of formalisations is that
wikis can be great for text (e.g. documentation, encyclopedias,
teaching notes, discussions etc.), but distributed version control
software such as monotone or darcs are best for code.
This is right, but is creating formalized mathematics more like creating documents or more like writing code? I would say that for people with computing science background it is more like writing code and for mathematicians it is more like creating documents. It is certainly more like creating documents for me.
Note that you can contribute to formalized mathematics projects the software way right now. If you send a sensible contribution to IsarMathLib you can get commit rights to IsarMathLib's Subversion repository (disclaimer: IsarMathLib is my project). I believe there are also COQ projects you can contribute to. The wiki way for formal math is different and new. It may not work but we will not find out until we try.
> attracting vandals and spammers
The IsarMathLib-like style that Cameron plans Vdash will use has interleaved informal and formal text. For informal text the problems with vandals and spammers are the same as with any other wiki. Formal text is easy to protect with some simple safeguards (like not allowing to remove or change the assertion of a theorem that other theorems depend on, I write about it in another post).
> By contrast, in a gatekeeper-mediated software project at
least some of the "burden of proof" (no pun intended) falls on the
submitter
No pun was intended, but really if wiki won't allow to save pages that are not verified, the burden of proof is on the submitter.
> encouraging people to use an interface - a wiki - which isn't, at
present, anywhere well enough integrated into a theorem prover (or other
formalisation tool).
This is a problem, but not as big as you may think coming from COQ.
There are to approaches for interaction when verifying the proof. On one side of the spectrum is COQ - you practically have to interact with the prover at every line. On the other is Mizar with its batch mode - you write and submit a whole proof and Mizar tells you which steps it didn't accept. Of course the batch mode is better for Wiki. Isabelle is similar to COQ in that it stops processing on the first error, but with some additional effort from the verification server it can get close to the batch mode. The server can send the theorems on a page one by one to Isabelle and if the verification of one of them fails it can retract it and try the next one. This would allow to get some information for all theorems, not only those before the first failing one.
> it might make more sense to force users to run them locally.
There is a big psychological difference between trying things on-line with immediate feedback and having to invest effort in installing Isabelle or another prover, before you can do anything.
> you need to learn a language and that takes time. If you've got time for that,
you've got time to install an .exe file,
Things are really different from the perspective of a person who does formal verification of software and an average mathematician. Isabelle doesn't even run on the OS that most people are using.
> "it needs to be dead simple to use" argument, because,
let's face it, theorem provers are *not* dead simple to use.
It looks like you are quoting but I don't think anybody here claims that writing formal proofs can be made dead simple. Wiki can remove some obstacles and make it more fun, but it always be harder than writing informal stories (I can't say "informal proofs" because that is an oxymoron) that aim to convince humans.
Slawekk
__________________________________________________
Do You Yahoo!?
Tired of spam? Yahoo! Mail has the best spam protection around
http://mail.yahoo.com