The Limits of Static Reasoning

Share the article!

20030611062447

Richard Gabriel in his arguments why “Objects Have Failed”, writes:

And as a result we find that object-oriented languages have succumb to static thinkers who worship perfect planning over runtime adaptability, early decisions over late ones, and the wisdom of compilers over the cleverness of failure detection and repair.

Beyond static types, precise interfaces, and mathematical reasoning, we need self-healing and self-organizing mechanisms, checking for and responding to failures, and managing systems whose overall complexity is beyond the ken of any single person.

Sean McGrath makes similar observations:

PI Calculus, the formalism that underlies some common Business Process Modelling languages, may have an interesting role to play in the static versus dynamic languages debate.
Lots of powerful techniques that can be used with PI Calculi involve using higher order concepts such as sending names of ports/channels over links, creating ports on the fly and so on.
This stuff drives the math heads nuts because it makes it hard (impossible?) to formally prove equivalence between calculi.
So it boils down to this – do you want to be constrained in terms of flexibility or provably, formally, “correct” at some probably academic level?
I’ll take flexibility thank you very much!
Advocates of Dynamic Programming languages like Python find higher order PI Calculi stuff completely natural and use test driven development as a more robust methodology for establishing “correctness” in this crazy, constantly changing, dynamic world.
Why not? The other approach – the keep everything static so that the compiler police can look over it – only provides the illusion of correctness. What have you to loose?
 

Both intersting and compelling arguments, I will admit, I agree with both of them!  That may sound as a shock to people who recall my piece on “Static vs Dynamic Typing” debate. I had sided with the “Static” side.  If you recall however, my arguments were not for more correctness rather it was a realization that being more explicit allows a compiler to do a lot of the thinking for you. That is, the navigation, auto completion, on the fly checking, quick fix capabilities that you find in Eclipse and IDEA outweigh the productivity benefits of any dynamic typed language.   People who program in both environments know this as a fact.

However, I’ve always advocated a loosely coupled architecture.  If you looked at the table I constructed earlier, flexibility is a motivation of loose coupling at the expense of correctness.  Furthermore, I had talked about ”programming in the large“, and that our notions of programming in the small can’t apply for larger systems.  In fact, I do have a prescription for this which I explained that a dynamic component model is necessary for any large scale system.

The limits of static reasoning can be found at the boundaries between the one author single machine application and the multiple author distributed agent ecosystem.  


Share the article!

Leave a Reply

Your email address will not be published. Required fields are marked *

You may use these HTML tags and attributes: <a href="" title=""> <abbr title=""> <acronym title=""> <b> <blockquote cite=""> <cite> <code> <del datetime=""> <em> <i> <q cite=""> <strike> <strong>