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