I don't like about Java and C++ (Static typing is just wrong!

Java and C++ are not really statically typed, in that they allow casts, in fact they require casts. This means that type errors can occur at runtime, which is exactly what static typing is supposed to prevent. Have a read MJD's excellent talk? You should read some ML or Haskell, you don't have get into monads to appreciate a lot of Haskell's typing system. I'm not even sure if I correctly understand monads because I haven't ever tried to write anything in Haskell but I can still appreciate what real static typing (with type inference so that you don't have keep telling the compiler things it could work out for itself) can do.

I think it's cecil that brings another rather cool feature to static typing, it lets you get it wrong but still compiles your code (issuing warnings of course). This allows you to experiment with your classes as in a dynamic language without having to rewrite half your code just to get it to compile.

So yes, Java and C++'s static typing is absolutely wrong but it's not really static typing.

Java and C++ are not really statically typed

They are not strongly typed, but they are statically typed. There is a distinction. Strong typing means you cannot easily convert between data types (for instance, Perl is strongly typed. It is not particularly easy to convert between an array and a scalar). Static typing means the types are determined at compile-time. Casting is what you have to do in C and Java to circumvent the static type checking.

If you look at MJD's excellent talk again, you'll notice it is saying that strong typing can be good. It is also describing why static typing, as implemented in Pascal and C (and by extension, Java), is not very helpful.

It seems to me that he is singing the praises of lanagues which are (according to your definitions) both strongly typed and statically typed.

His Spectacular Example shows ML detecting an infinite loop at compile time (ie statically) but ML's fancy static type system wouldn't be much better than Java's if it wasn't also strong (that would essentially be Java + type inference, allowing you to cut out lots of declarations but still leaving you open to run time type errors). Strong without static would be Perl and that talk is definitely not a celebration of Perl's type system.

The definitions are controversial and somewhere (possibily in that or another MJD talk) there's a list of about 8 conflicting definition for various kinds of typing but in that talk, on this page he says "static" and "strong" typing are the same.

If you really want to make a distinction you could take "strong" to mean that conversions (casts) are impossible and "static" to mean that types are determined at compile time. Then, if you want to say that Java really is statically typed you should probably make it clear that you mean that "types are determined at compile time but might have been determined incorrectly". Come to think of it, that's a great definition, it makes it clear just how badly Java, C, and C++'s type systems suck.

Maybe we should call Java a "hopefully typed" language :-).

If you like Java's type checking, you'll love any language with a modern Hindley-Milner type system. (Haskell is one; I believe OCaml is another.) My mental model of this type systems keeps evolving; right now it's something like a lightweight OO system with easy and unambiguous multiple inheritance, augmented with recursive typing. Of course I despised it when I started writing Haskell -- I was used to the Lispy "lots of conses" method of functional programming -- but it's grown on me.

--
Yours in pedantry,
F o x t r o t U n i f o r m