On Tuesday 29 May 2007 12:40 pm, Lex Spoon wrote:
> Yes, algorithms are more amenable to proof than implementation.  If
> you implement a proven algorithm, and something goes wrong, then it's
> a normal old bug.
Proofs and Implementation represent two ends of a large spectrum. Algorithms 
falls there somewhere in between (but closer to Proofs). I think Alan Kay 
pointed out a few mails before that "HW is just SW crystallized early". A 
mathematician would work near the Proof end, while an engineer would have to 
tackle the Implementation side. For engineers, any system that takes 
us "close enough" is good enough.  But, algorithm to implementation is a big 
leap of faith today :-(. Where the translation covers just a couple of orders 
of magnitude (e.g. math, graphics etc), we can achieve an accuracy that is 
sufficient to commit to HW. But, where modularity is introduced at compile 
time but vanishes at runtime, we are forced to analyze code that runs into 
millions of machine instructions. Bugs will be the norm rather than an 
exception :-).

Projects like Exupery are good because they help us short-circuit many steps 
between algorithms to machine instructions. The first Smalltalk machine 
description didn't come with invariants and the bugs were discovered 'at 
execution time' (cf. Bits of History). It would be interesting to see if 
Dynabook could be described in Smalltalk along with all invariants.

Regards .. Subbu