[Top][All Lists]
[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]
Re: [Axiom-developer] LogiWeb
From: |
Ralf Hemmecke |
Subject: |
Re: [Axiom-developer] LogiWeb |
Date: |
Sat, 30 Jun 2007 02:06:25 +0200 |
User-agent: |
Thunderbird 2.0.0.4 (X11/20070604) |
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.
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.
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). 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.
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.
LogiWeb is GPL. The only drawback I see is that it is basically a
one-man-project. And I am still not clear about what it really means to
program in pure lambda calculus. It sounds a bit scary to me, but maybe
it's a good thing.
Ralf
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.