An approach for implementing TUNES

[Brent Kerby]

> 
> In short, you propose that we design by contract, and that we build a
> tool for finding implementations of a given contract. 
> 
> Laurent

Exactly. Of course, in a way, all programming languages that I know of are
somewhat like this. For instance, if you program in C or assembly, you
write specifications about your program and then use a tool, a compiler or
assembler, to find an implementation (i.e. machine code, or marked-up
machine code like EXE or ELF) given that specification. The difference is
that using the logic tool you could define TUNES (or at least state enough
about it for the tool to reason about it), while you could not in C or
assembly without resorting to overspecification (giving more details than
you really need to), and even then, it would be a big pain to do it in C or
assembly.

But still, remember that the tool would only be for implementing TUNES. It
would be thrown away after TUNES was implemented because we'd already have
something twice as good. TUNES itself will no doubt include a logic system
similar to the one I've described, because it is _so useful_. For instance,
if a user wanted to know what X was, given that "X*X + 3X + 10 = 0", he
would just ask TUNES, and TUNES would tell him. In contrast, without the
logic system, we'd have to arbitrarily implement solving of quadratic
equations in TUNES (which would be foolish, because there are so many other
similar situations that would turn up), or the user would have to dig up
his math book and recall the quadratic formula, then write a procedure or
something for it, then use the machine only to do the brute computation,
when it could have done so much more.

Because TUNES itself will need a logic system, we will either need to
hand-code the logic system when writing TUNES some other way, or we will
need to hand-code a prototype logic system which we will use to find TUNES
(including the TUNES logic system). I think the latter would be much much
easier, because the logic system could then be used to automatically
implement device drivers, memory management, and all that other stuff that
we'd otherwise be a pain to hand-code into TUNES. Also, even when TUNES is
finished, when can keep our original definitions of TUNES and our target
machines (even though we will throw away the tool that originally used
them). Adding a new target for TUNES would be a mere matter of specifying
the behavior of the target and possibly making a few adjustments to the
TUNES definition to adapt to the new target's hardware abilities. A working
TUNES could then be used to find a disk image that would work for the new
target.

More comments are welcome...

- Brent Kerby ("Iepos")