Re: [Axiom-developer] LogiWeb

[Klaus Ebbe Grue]

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