Roel Wuyts <roel.wuyts at iam.unibe.ch> wrote:
	To put it slightly differently: there is currently no static typing 
	system that you do not have to give 'hints' (using typecasts) since you 
	know better than the system what is going on.

Wrong.  Haskell and Clean, for example, have strong static polymorphic
typing and don't have any kind of typecast.  It has been a while since I
last used O'CAML, which has basically a Hindley-Milner typesystem extended
to cope with extensible records (read: OOP), but I don't recall any
typecasts in O'CAML either and I've certainly never needed any.

The problem is, you are confusing C/C++/Java constructs with *real*
type systems.

	Most mathematicians working in this area only consider
	object-oriented languages where you have no polymorphism :-)
	
I'm not sure how to react to that.  There's a _lot_ of theoretical
computer science on type systems for polymorphism, and if you want
"real" (meta-)mathematics, Martin-L\"of's type theory has handled
polymorphism (via dependent types) for a long time now.

Java's type system isn't state-of-the-art and wouldn't have been 20 years ago.

I like Smalltalk/Prolog/Erlang/Lisp a lot myself.  I'm not knocking them.
But DON'T for heaven's sake use Java as a stick to beat "static typing" with.

As for C++, I'm not sure what to make of a language where the question
"are these types the same type" doesn't have a decision procedure.
(That is, there is no algorithm which always correctly returns "yes" or
"no" in a finite time.  The C++ standard explicitly allows C++ compilers
to be 'incomplete' when it comes to calculations about types, in effect,
in order to give an answer in a finite time, the compiler is allowed to
give the _wrong_ answer.  Problem is, different compilers may give
_different_ answers.)  Again, don't use C++ as a stick to beat "static
typing" with; there are static type systems which are more expressive
and less trouble.