An approach for implementing TUNES

[Francois-Rene Rideau]

[About specifying a PC]
> Well there would be no need to specify the mysterious parts of it (although
> doing so might give the logic system the ability to make a more efficient
> TUNES).
Well, indeed, we may usefully under-specify the system,
since we're only interested in states reachable
from legal Tunes-compiled programs.

>> People wanting 100% proven systems will better pick
>> [a better archicture than the PC]
> 
> Well... certainly there are better-designed systems than the good ol'
> IBM-PC, but there are so many ibm-pcs out there... Besides, the fact that
> emulators like "bochs" have been written shows that it is possible, because
> certainly it would be easier to write a specification than to write an
> emulator in C. btw,

>> (btw, the people at CLI have proven the design of a 32-bit processor
>> of theirs using ACL2).
> what is CLI and ACL2, and what does it mean to prove
> the design of a processor?
Computational Logic, Inc. is the company founded by the famous
Bob Boyer & J Strother Moore (ever heard about boyer-moore? should!)
ACL2 -- A Computational Logic - Applicative Common LISP
is the modern continuation of their fantastic theorem prover Nqthm.
	http://www.cli.com

> Hmm... As I said before, specifying a PC, although far from trivial, seems
> fairly practical to me.
Well, you have convincing arguments that it is not only possible
but actually feasible. The difficult part is now to find the proof system
infrastructure in which to do it, that we can later integrate to Tunes...

> I guess I've actually been talking about a subset of a
> PC specification the whole time... We don't need specification of those
> model-dependent-registers or whatever they're called on the new processors,
> or any other freaky features that you can find on most hard disks, video
> cards, etc..
The problem is, you might have to, for some purposes, though not for others.
For instance, proving the correctness of the persistent store requires
a model of the hard-disk system (well specified with SCSI; not so with IDE).
Proving the correctness of drawing routines requires a model of the video
(beware that things are often not exactly the same when done by the video
hardware, and that discrepancies should "leak" into a security breach
when misspecifying what happens with video or other inexact I/O).

> Wouldn't it be possible for a proof system to _generate_ a
> compiler using the definition of the language and the definition of a PC
> subset?
Yes and no. There is no canonical compiler, even less a canonical way
to get an *efficient* "optimizing" compiler; however, there are ways
to specify compiler-generating "tactics" that are known to be correct
independently from the parameters chosen to "tweak" the compiler efficiency.
I believe the Proteus project at UNC had this in mind.

> I don't quite understand what you mean by a "level of abstraction".
> Do you mean at various levels of detail?
Yes, but by saying "abstraction level", I imply some consistent
structuration among the properties ("details") that you consider
at any given moment.

> It does seem like generalizing (increasing the
> level of abstraction?) would make proof easier.
Every proof is made easiest by choosing the highest level of abstraction
that fits. Actually, the interesting theorem is often the one that proves
the correctness of the change in point of view (or successive changes)
from the one in which the problem is stated until the one in which it
becomes trivial.

> It is easier to reason
> about things when you have less detail to worry about; so it is best to
> find a pattern in the detail and describe in simpler but more abstract
> terms. Is that what you mean? I don't understand how that's the same as
> reflection though (self-modification).
That's exactly what I mean, and precisely what reflection is all about:
chosing the right abstraction level at the right moment,
by fully deconstructing (reifying the semantics of) an object
to interface it with low-level metaprograms when details are needed,
and by quotienting it (forgetting the irrelevant) when details
are no more needed.

>> So in practice, it looks like we'll have to begin with empty
>> specifications and lots of axioms, and slowly specify things.
> Yes, I guess that is the equivalent of writing TUNES in assembly or C,
> making lots of vague assumptions (axioms).
Exactly. Of course, when we begin massively specifying things,
we may have to completely reimplement "dirty" parts of the system
so as to be able to achieve provable code.

>> Maybe it'll end up being easier, on the contrary, to specify things,
>> and let metaprograms deduce the code automatically from proofs:
> Yes, that's exactly what I'm suggesting. It certainly would be easier, if
> only the "metaprogram" could be written. Anyhow, TUNES will not be complete
> until it includes such a metaprogram.
I fully agree. However, for early bootstrap versions, we do not yet
have the proof system infrastructure.

> What is a "pure computation".
Computation without side effects. See ACL2, Coq.
See Haskell, Clean, Mercury.

> Are you talking about lambda-calculus or
> combinatory logic reduction.
For instance.

> Would solving a quadratic equation be a pure computation?
Any computation can be expressed in a pure way,
and even side-effects can be described in a pure way, with monads.

> Hmm... What is Meyerish d-b-c?
Design-By-Contract as described by Eiffel inventor Bertrand Meyer
(an annoying guy who has a few good ideas, but doesn't quite understand
the lambda nature).

>> express and check runtime decidable properties, whereas we want to deal
>> with arbitrary provable properties.
> Hmm... what is a runtime decidable property?
I mean, runtime checkable properties.
Eiffel-like contracts are no more expressive than C assertions.
They are just a clean, systematic, and optimizable way to do assertions.

>> 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).
> 
> I don't quite follow that last statement...
When you type " 2 2 + " or any other command at your prompt,
the only a priori specification is that the computer should return
the correct answer; hence, this is no different from another system.
Proofs don't come to annoy you unless you specifically ask for them,
because you need them or want them.

[ "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 ]
First they ignore you. Then they laugh at you.
Then they fight you. Then you win.
	-- Gandhi