Florin wrote:
>..I would say though that math looks to me like it
>is still ticking,

An interesting thing about math/logic is that it can prove some of
it's own limitations.

I think I remember hearing about proofs of the insolvability of the n>2 body problem
and of general solutions to finding the roots of polynomials above a certain order.

If these problems are provably insolvablable, should we have much
confidence in what seem to be the more complex problems of large programs
being solvable? (By solvable I mean knowing everything about what they
do without actually running them)

I think most everyone sees that complex programs (like n>2-body problems)
can't be analyzed without computation, so there are two choices.

The top-down approach is to attempt to make programming langagues more
analyzable before computation (Strong typing, etc) so correctness can be proven.
This approach is basically out to eliminate the dynamic aspects of the system
that lead to complexity. (Of course if Smalltalk can be written in ADA, how
is ADA more provably correct or "safe"?)

The bottom-up approach is to look for new ways of managing complexity so correctness
is more probable. OO of the Smalltalk type is, IMO, an example of the 2nd approach.
It looks at real the source of chaos - excessively coupled equations (via variables)
and structures the langauge to make this problem easier to avoid.

So while the top-down thinkers are unsuccessfully trying to make correctness provable,
the bottom-up thinkers are successfully making correctness more probable.

Steve