is Java getting close to Ada strong type checking with this tool?

[peteclose@- <peteclose_member@newsguy.com>]

http://research.compaq.com/SRC/esc/

"The Compaq Extended Static Checker for Java (ESC/Java), developed at the Compaq
Systems Research Center (SRC), is a programming tool for finding errors in Java
programs.  ESC/Java detects, at compile time, common programming errors that
ordinarily are not detected until run time, and sometimes not even then; for
example, null dereference errors, array bounds errors, type cast errors, and
race conditions.

ESC/Java uses program verification technology, but feels to a programmer more
like a type checker.  By using an underlying automatic theorem prover, ESC/Java
is more semantically thorough than decidable static analysis techniques.  At the
same time, because it tries to detect certain kinds of errors only, and not
prove the program's correctness, the technique is more automatic than full
functional program verification. "