An approach for implementing TUNES

[Francois-Rene Rideau]

>>: Faré
>: Iepos

[Specifying a PC]
> Yes... would it be possible to do it in Coq or ACL2?
Well, yes it would. However, both Coq and ACL2 have enough idiosyncrasies
that such a specification would be very hard to use outside of them,
which would make it very difficult for proofs in such systems to be used
as a way to program Tunes, unless you port and encapsulate said proof
system in Tunes (or the other way round), which would both be a lot of
work, and a very dear constraint to put on Tunes.

The interesting question is of course, would this work and these
constraints cost _more_ or _less_ than beginning a new proof system
from scratch? I *think* the answer is that it would cost _more_,
for essentially one reason: I want that Tunes be a reflective
metaprogramming system, and none of the existing formal logic systems
that I know of can be easily expanded towards that direction in a sound way.
Actually, ACL2 has its own kind of reflection, but a very specific one that
doesn't fit a larger category of metaprogramming that I wish for Tunes,
whereas Coq (and other LCF descendants) has metaprogramming in ML,
but it is not quite reflective.

>> 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).
> It certainly does, but that does not mean we have to specify useless
> extensions to the IDE standard. We only have to specify enough so that a
> working TUNES system with a persistent store can be found by the logic
> system.
Well, the problem with IDE is precisely that, by lack of specification
on the way buffers are flushed, failsafe persistence is not implementable
(contrarily to what is the case with SCSI), unless you're ready to make
a lot of blind assumptions (hopefully correct guesses) that bring you in
the safe zone. Of course, even if you don't formally specify the standard
and your additional assumptions, you're still using it and making them.

My point is that specification is a difficult task that cannot be done
correctly outright; programming proven-correct things with evolving
specifications is an even more daunting task. These tasks require tools
that just do not exist currently. It is also the goal of Tunes to bring
those tools. But we might have to rely not on these tools to bootstrap
Tunes.


>> 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).
> 
> That is true... If we specify that operation FOO only puts a pixel on the 
> screen, when it actually makes the monitor blow up, then anyone who the 
> security privilege to put a pixel on the screen will be able to perform 
> operation FOO and thus make the monitor blow up.
>
The problem is much more subtle: if you formally define "drawing a line"
by a given routine, but the actual hardware or library routine will
draw the line in a different way (displacing a few pixels,
doing anti-aliasing in a different way, etc), then there will be
a discrepancy between your assumptions and the reality,
and an ill-intentionned user or a ill-driven program
might use this discrepancy to prove an absurdity in your system,
whence to be able to have the system admit any inconsistent axiom.

Specifying operations as conceptually "simple" as "drawing a line"
in a way that be both correct and useful is _quite_ challenging!
The same could be said of "real number" arithmetics, all the more
when you want to relate your "real" arithmetics implementation (IEEE or not)
to approximations of actual mathematical numbers.
Again, this does NOT mean that the task is unfeasible:
when people design programs so as to be correct,
they do, in their right mind, do this work of relating
implementations to specifications,
so that, when programs are actually correct,
there _is_ a way that could be found to prove it.
But this is nonetheless a very complex task for which tools
are currently lacking.

>> 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.
>
> I think i kinda get what you're saying. I'd like to see an example
> of such a proof.

A very well-known example of a theorem people use to demonstrate their
favorite proof system is REVERSE-REVERSE: to reverse a list (structure
inductively defined from cons and nil) is an involutive operation.
Well, the elegant and interesting way to do this (I think) is to
prove that the free inductive presentation of lists with cons and nil
is isomorphic to the presentation of lists as either the empty list,
or a non-empty one, with non-empty lists being inductively defined
from atom and append, with the equations making append associative.
Once you have this equivalence between two points of views,
the non-trivial theorem REVERSE-REVERSE among cons-nil lists
becomes a trivial theorem about (recursively) commuting the arguments
to append among nil-atom-append lists.
Similarly, many fundamental theorems in every field of mathematics
consist in proving the equivalence between several ways to define
a "same" structure.

>> [this is] 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.
>
> Again, I think i might understand what you're saying, but a simple example
> would be nice.

Hum. I'm going to write (yet another) article right about that.
One I should have written long ago...


>> 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.
>
> Yes, we would. But I am still wondering if we can escape writing any 
> "dirty" code at all, by finding or writing a logic system to find a TUNES,
> giving the TUNES definition, and the definition of our target.
>
You seem to ignore that writing a logic system, or adapting one so it
be reflective, _does_ include a lot of dirty work!

[ "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 ]
Reality must take precedence over public relations,
for Mother Nature cannot be fooled.
		-- R.P. Feynman