Sun Oct 4 11:54:03 CEST 2009
The Two Towers.
Two important things happened to me in the course of the last 10
years. Rising from the puddle of asm and C, I discovered Forth and
its algebraic nature, and Scheme, lambda calculus, macros, types, ...
The practical pilar was compilation.
Through manipulation of language as just another data object, a
different kind of math was brought within my reach - quite different
than the isolated world of linear algebra and calculus useful for
numerical applications. Instead of math being something that's done
on paper, it came to live in my hands through the manipulation of code
This took a couple of years to really sink in. As opposed to the
principle being simple - formal languages, axioms and inference rules,
semantics represented by functions mapping language objects to
other objects, there is an incredible range of possible ways to bring
mathematical structures to physical computing machinery.
So is logic the ultimate programming language? I guess it depends on
what your goals are. Currently I see really only two camps in
software development: the mathematical / logical camp which limits
power by introducing formal abstractions that have provable or
verifyable properties, and the biological camp which uses evolutionary
techniques to approach correctness (and specification!) by removing
constraints and looking only at observable behaviour.
I guess the point is something like this: since computers themselves
behave mathematically (within certain bounds), do you want to
propagate this kind of exactness to very high level claims (proofs in
logic), or are you more interested in using the computer to give you a
system that implements limitless power (reflection / programmable
Maybe, stretching it a bit, the former could be called the tree /
directed graph approach (proof / transport of truth), while the other
is the full graph approach (connected objects, the internet model).