a few queries

[Andrew J. Blumberg]

you flame a lot about proofs and parallelism. . .

with all due respect, i don't think the solutions to our computational
problems are quite as straightforward as you tend to suggest.

for example, proofs are spiffy --- when you can find them.  but proof of
correctness is intractable in general and often hard in the specific case.
. . there's been a fair amount of work in automatic proof generation
without tremendous successes; the theorem-provers i'm aware of are fairly
slow even in soluble cases.  and requiring the programmer to prove
correctness seems rather draconian. . .

as far as parallelism goes, exactly what parallel model do you support?  it
sounds like you advocate something like a connection machine style model. .
. in any event, using large-scale parallelism well is another hard problem.
. . especially given that these days the speed of the processor is vastly
faster than the speed of the routing network.  sure, it would appear that
parallel processing is a winner, but there are a lot of problems for which
it is not at all clear how to split the problem up. . .

i'm not trying to attack you so much as point out my uneasiness with your
rather glib discussions of issues that don't appear to me to be at all
trivial.

                                                                - andrew