An approach for implementing TUNES

[Iepos]

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

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

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

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, what is CLI and ACL2, and what does it mean to prove
the design of a processor? 

> All in all, unless there is specific funding about it,
> I don't expect anyone to fully specify a PC.

Hmm... As I said before, specifying a PC, although far from trivial, seems
fairly practical to me.

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

It certainly would. 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.. 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?

> 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

I don't quite understand what you mean by a "level of abstraction". Do you
mean at various levels of detail? (i.e., being able to reason about the
electrons flowing through the processor and the CRT and photons escaping,
but also about being able to reason at a higher level about the
instructions being executed and the state of the monitor in terms of maybe
a matrix of RGB pixels). It does seem like generalizing (increasing the
level of abstraction?) would make proof easier. 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).

> (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!

I have never used Coq or ML. I'll have to try it out sometime.

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

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

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

I read part of that a while back, but couldn't really understand it. I'll
have to look at it again sometime.

> as well as my masters thesis (in french) somewhere under
> 	http://www.tunes.org/~fare/files/

Hmm... maybe i should look at that too, mais mon francais n'est pas trop
bon.

> However, 1) my articles give no hint towards an efficient implementation
> and 2) like most proof systems, they only tackle pure computations.

What is a "pure computation". Are you talking about lambda-calculus or
combinatory logic reduction. Would solving a quadratic equation be a pure
computation?

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

Where are they, where are they? Side-effects? Well, side-effecting
functions are not really functions at all. Systems that make no clear
distinction between functions and procedures are not too good, but a system
that cannot perform any action other than computation and minimal user
interface is pretty limited too. 

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

Hmm... What is Meyerish d-b-c?

> express and check runtime decidable properties, whereas we want to deal
> with arbitrary provable properties.

Hmm... what is a runtime decidable property? 

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

Anyway, thanx for your comments... More are of course welcome...

- Brent Kerby ("Iepos")