On Sunday 27 May 2007 1:32 am, Lex Spoon wrote:
> 1. 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.

> 2. 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