[Top][All Lists]
[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]
Re: [Axiom-developer] LogiWeb
From: |
Klaus Ebbe Grue |
Subject: |
Re: [Axiom-developer] LogiWeb |
Date: |
Tue, 3 Jul 2007 09:19:41 +0200 (CEST) |
Hi Ralf,
http://logiweb.eu/
That seems to be a very interesting project.
Yes it does seem both interesting and relevant to Axiom but I hope
that the talk was easier to navigate and to understand than the above
website! It took me a long time to decide that this was indeed
something interesting.
I am sorry that I did not write more.
So am I :-)
The fundamental problem of constructing a web-site for Logiweb is that
Logiweb can suit more than one need. It is difficult to target a
web-site since there is more than one possible audience.
But if you explain what you are doing (e.g. giving an URL I should start
with), then I would be able to say something about whether or not Logiweb
would be helpful to you and, if it is, how it could be used.
When you have a chance, could you try to (briefly) summarize the talk?
Or do you have a link to a more readable introduction?
In fact, I was at the talk more by accident than actually planned.
What I got from the talk is that LogiWeb is actually more of an
infrastructure than anything else. But it does seem to have some connections
to proof systems.
Yes. It is an infrastructure more than anything else. One can publish
'pages' (or 'papers' or 'pamflets' if you like) on it. Such pages can be
flat TeX, but they may also contain programs, lemmas, proofs, and similar.
A page can also define what to do with formal contents (e.g.: compile the
programs, run programs on specified data, render the output, invoke
particular proof systems on particular proofs, and much more).
But instead of explaining everything the system can do, it would probably
be more efficient if I understood your needs first and then targeted the
explanations to your needs.
Think of the Axiom Journal idea. From the talk I thought that LogiWeb
implements a lot of that idea. It is, in fact, a revision control system (I
would say very much like GIT, but maybe Klaus Grue can say more about it).
I would be happy to. Could you give me the optimal URL (http://git.or.cz/
?) to start with.
LogiWeb allows to write and publish papers that contain formal mathematics
and a way to specify a proof system that actually checks the correctness of
the paper (including the referenced papers). There is no connection to CAS
yet, but maybe that can be changed.
Which CAS do you mean? Maybe, again, an URL would be the right thing to
start with.
An Axiom Journal for me is like LogiWeb only that the papers are our
pamphlets and that we need a compiler that actually compiles the referenced
pamphlets into a running Axiom with an appropriate library that is relevant
for the paper you are currently interested in.
There are questions like how to make sure that a paper that is runnable
today would run also on some computer in 5 years. I still don't know how to
achieve this properly, but Klaus Grue seemed to have ideas about it.
There are two ways to do that in Logiweb:
(1) Since Logiweb can publish programs and since proof systems are
programs, Logiweb can publish proof systems. In that way the proof systems
get under version control of Logiweb (that is why I bugged Andrzej
Trybulec to release the Pascal sources of Mizar). Once a proof checker
gets under version control of Logiweb, each Logiweb 'page' can specify
which version of which proof checker should check the proofs. When a
program is published on Logiweb, that program can be run as long as
Logiweb itself is ported to future systems. But it requires the program
to be expressed in a way Logiweb can understand.
(2) A poor mans version is to register one version or a small number of
versions of a proof checker as external programs which can be invoked by
Logiweb. That is quick to do and a good way to get started, but I am not
sure it would be a good idea in the long run.
LogiWeb is GPL. The only drawback I see is that it is basically a
one-man-project.
That is a decision I made. I have led several small and big software
development projects in academia as well as the industry. But Logiweb is
made the Knuth way: if you cannot program it yourself, it is too
complicated. There not one character in the source code that I have not
typed myself. The Knuth approach takes time, but the result tends to be
small and coherent.
But from now on, anyone can continue the developement of the system
without touching the source code: Anyone can add facilities to Logiweb by
publishing Logiweb pages containing the facilities. I intend to continue
doing bugfixes, minor updates, and porting (and I would not mind getting
help on that:-)
And I am still not clear about what it really means to
program in pure lambda calculus.
It means that if you want to define e.g. the factorial function, you would
reference a page (typically the 'base' page at logiweb.eu) which defines
numbers, Booleans, pairs, exceptions, addition, multiplication, etc. in
lambda calculus, and then you would write e.g.
x ! == if x = 0 then 1 else x * ( x - 1 ) !
Other programming languages can be supported. In particular, I will
support Pascal if the Mizar sources are released. And anyone can add
support for any language by publishing a Logiweb page which tells Logiweb
how to do. But, on Logiweb, anything ultimately compiles to lambda
calculus (at least in principle).
It sounds a bit scary to me, ...
It is, for the one who has to implement the low level details. You should
not bother.
but maybe it's
a good thing.
The benefit of having everything compile to lambda calculus is
that then one can, at least in principle, reason about any published
program just by reasoning about lambda calculus.
PS For Klaus Grue: A pamphlet is a file that apart from mathematics and
design decisions etc. also contains code that can be compiled. I somehow have
the suspicion that a pamphlet could be seen as a logiweb paper if our
underlying programming language were pure lambda calculus. But we want to use
some higher level language like Aldor/SPAD.
It sounds like very much the same. Could you give a good starting URL to
Aldor/SPAD (maybe www.aldor.org for Aldor?). Then I will take a look at
it and see if it would be easy to support. Programming languages can
always be supported the 'poor mans way' of course, having the compiler for
the language as an external tool.
Cheers,
Klaus
- Re: [Axiom-developer] LogiWeb,
Klaus Ebbe Grue <=