On Sunday 27 May 2007 1:32 am, Lex Spoon wrote:
- Even when you are thinking about formal proof, like Dijkstra was, parallelism in large OO programs means you have to reason about aliasing, i.e. you have to do data flow analysis. This is hard, probably too hard if the language is unconstrained.
What is hard about programming is coming up with the right invariants. What happens between the starting invariant and ending invariant is determined by the semantics. E.g. x, y := y, x is easier to reason about than bringing in a temp to swap x and y.
- Most programs are not formally proven.
True. Proving large programs automatically is theoretically infeasible for most languages in use today. But many algorithms do go thru formal proofs before adoption - e.g. floating point math, semaphores, regular expressions are all based on proven algorithms.
Instead, their correctness relies on careful reasoning, on good processes, and on testing. Parallelism undermines the testing part.
Testing invariants is not affected by serial/parallel execution, but debugging or tracing parallel programs is not really for faint-hearted :-).
BTW, this thread is veering off-topic. We should get back to the cost of Dynabook before Brad Fuller starts reaching out for a 2x4 :-).
Regards .. Subbu