Re: [Axiom-developer] LogiWeb

[Ralf Hemmecke]

> > 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.