in reply to Re^6: "strong typing" is potentially ambiguous
in thread (Completely OT) - Hero(i)n programming language on Slashdot

I don't think Pascal-derived type systems are useful for showing program correctness. They are only good for providing hints to the compiler.
Well, some people are doing some very interesting research into proof carrying code in java...

A Proof-Carrying Code Architecture for Java

An Overview of Proof-Carrying Code

-- All code is 100% tested and functional unless otherwise noted.
  • Comment on Re^7: "strong typing" is potentially ambiguous

In Section Perl News