An approach for implementing TUNES

[Billy Tanksley]

I hate Outlook.

> -----Original Message-----
> From:	Francois-Rene Rideau [SMTP:fare@tunes.org]
> Subject:	Re: An approach for implementing TUNES
> 
> 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:
> 
	Agreed.

> _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.
> 
	I wouldn't expect anyone to fully specify the ANSI C programming
language, but that's exactly what the abstract state machine people have
done.

> 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.
> 
	I know of one person who's doing this at the machine-code level (you
can't use anything higher level, because you don't know that the compiler
being used to compile the high-level language is itself correct).

	Add together his formal proof of a compiler's correctness, and the
ASM group's formal definition of a language (currently C, Prolog, and
Oberon) and resulting proof of a library, and you could be as formal as you
wanted.

> 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
> 
	Have I mentioned ASMs yet?  They are quite good at this, even
thought they're formal modelling systems rather than proofs (you have to
construct your own proof of the model).  Another interesting thing about
them is that they execute on the same time scale as the real system -- one
step per algorithm step.

> [ "Faré" | VN: Уng-Vû Bân | Join the TUNES project!
> http://www.tunes.org/  ]
> 
	-Billy