Alain Ketterlin <al...@universite-de-strasbourg.fr.invalid>:
> Your claim essentially is: since we cannot prove everything, let's not
> even try to prove anything. Go on if you think this is the right way to
> think about typing.
This discussion is far too metaphysical.
Static type declarations give you something at a cost. They give you:
* Performance (by several orders of magnitude).
* Static type checking (-> better quality).
* More code to type (-> worse quality, lower productivity).
In my experience it is far easier to produce correct code in Python than
in, say, C++ or Java.
Back to metaphysics: OO has spent far too much energy in ontology. You
shouldn't judge an object based on the class it belongs to.