An approach for implementing TUNES

[Francois-Rene Rideau]

BK>>: Brent Kerby

BK>> I think that both definitions (the behavior of an ibm-pc and
BK>> a TUNES system) would be quite feasible to write.
Feasible, certainly, but very costly:
_full_ specification of a PC is a particularly ungrateful task,
since every particular implementation has its own extensions and bugs.
People wanting 100% proven systems will better pick a simpler,
more robust, and better designed architecture (btw, the people at CLI
have proven the design of a 32-bit processor of theirs using ACL2).
All in all, unless there is specific funding about it,
I don't expect anyone to fully specify a PC.

However, formal specifications of the PC subset being actually used
might be interesting; it would be particularly useful in allowing
formal proofs of compiler correctness.
Doing it feasibly requires the possibility to consider the hardware
at various levels of abstraction (=reflection), which current proof systems
don't allow to do in a practical way. For instance, I'm familiar with Coq
(although Coq has evolved quite a bit since I last used it),
but it won't allow you to do safely and internally the proof
transformations needed, although you can do metaprogramming in OCAML.
Eat flaming death, non-reflective mongrels!

So in practice, it looks like we'll have to begin with empty specifications
and lots of axioms, and slowly specify things.
Maybe it'll end up being easier, on the contrary, to specify things,
and let metaprograms deduce the code automatically from proofs:
indeed, specifying means that we make our assumptions explicit,
and implies that we understand better what we do,
and helps avoid otherwise unfindable bugs whose squashing would require days.
Only by doing will we find.

As for a fully reflective proof systems, see my lambdaND article in
	http://www.tunes.org/~fare/tmp/
as well as my masters thesis (in french) somewhere under
	http://www.tunes.org/~fare/files/
However, 1) my articles give no hint towards an efficient implementation
and 2) like most proof systems, they only tackle pure computations.

BK>> However, I have almost no idea how to implement the logic tool. Once
BK>> again, I ask, does anyone else know how?
Well, there are plenty of examples to inspire from,
although none that deals directly with side-effecting code.

LM>: Laurent Martelli
LM> In short, you propose that we design by contract, and that we build a
LM> tool for finding implementations of a given contract. 
No, it's more than design-by-contract, because Meyerish d-b-c can only
express and check runtime decidable properties, whereas we want to deal
with arbitrary provable properties.

As for Laurent's original question:
>>> Can you give us an example of how you'd do "hello world", ` 2 + 2 ', or
>>> something simple ?
I will be just the same as in another system:
because in everyday computations the only specification you give
is that the computer should obey the orders correctly.
You begin to use specifications when you want to impose an invariant,
and/or to pass a contract with someone else (or a past or future self).

[ "Faré" | VN: Уng-Vû Bân | Join the TUNES project!   http://www.tunes.org/  ]
[ FR: François-René Rideau | TUNES is a Useful, Nevertheless Expedient System ]
[ Reflection&Cybernethics  | Project for  a Free Reflective  Computing System ]
In a five year period we can get one superb programming language.
Only we can't control when the five year period will begin. -- Alan Perlis