Tunes 0.0.0.34

[Fare Rideau]

Dear Tunesers,

>>: Fare
>: Billy

>> PS: have you seen the ACL2 theorem prover? Impressive -- has been used
>> to prove correctness of part of all of actual CPU designs,
>> as well as theorems in higher mathematics...
>> 	http://www.cli.com/software/acl2/v1-9/
>
> Facinating.
>
Oops. My fongue torked. Of course, you all corrected implicitly;
still let me apologize and clarify things.
   I really meant "(part or all) of (actual CPU) designs",
i.e. a few actual CPUs were specially designed to be completely proven
from ground up (assuming the fab process did implement the
intended semantics for the description language),
while the prover was used for parts of other designs.
   For instance, AMD had its K5 FPU microcode proven correct after the
scandal about a Pentium FDIV bug (other parts of the K5 were not proven
or even analyzed, and are indeed known to be buggy; dunno about the K6).
   Obviously, formal methods weren't used for all of actual CPU designs,
or the kind of design bugs we know would be
"bai now jast a memori in the maindz ov ould doderez" [fortune -m Twain].
Still I'm sure they would only leave place for quite rarer but rather subtler
and more difficult to solve meta-bugs.

-- #f, now (I hope) with a working .procmailrc, until next time...