not safe at all

[Alex Martelli]

"Quinn Dunkan" <quinn at yak.ugcs.caltech.edu> wrote in message
news:slrn9kui1i.orp.quinn at yak.ugcs.caltech.edu...
    ...
> The static people talk about rigorously enforced interfaces, correctness
> proofs, contracts, etc.  The dynamic people talk about rigorously enforced
> testing and say that types only catch a small portion of possible errors.
The

Although "programming by contracting" was historically developed in
the static-typing community, no significant contract in PbC is enforced
statically in (e.g.) Eiffel, the summit (according to its adherents) of
both static typing and PbC.  Preconditions, postconditions, and class
invariants, are typically rich and complex sets of expressions and no
real-world compiler is able to check anything but very trivial subsets
of them at compile-time.

So, IMNVHO, contracts should NOT be placed in the "static typing" camp,
although it IS true that static typers do tend to talk often about them.
What PbC's practice proves is that DYNAMIC enforcement is just fine
for the really important issues -- sure, sure, it would be an even better
world if we COULD check a few more things even earlier, but wtf -0- we
can't, and PbC still helps.  Dynamic strong typing -- THAT is what PbC
turns out to be in practice.  And a durned fine thing it is, too!

Actually, I wouldn't mind an 'assertion language' that's not even
truly checkable (fast enough to be useful) at runtime -- one where
I could use existential and universal quantifiers, because those are
so often the things I *WANT* to express in a formal, unambiguous
way.  Consider the predicate parameter P I can pass to many of
the containers and algorithms in the standard C++ library.  What
I often want to assert about the type of P is: for all X, not P(X,X);
for all X and Y, P(X,Y) implies not P(Y,X); for all X, Y and Z,
P(X,Y) and P(Y,Z) imply P(X,Z).  I.e., the crucial facts about P's
type is that it's antireflexive, antisymmetric, transitive.  What I
_can_ assert that's static-type-checkable is that P accepts two
"foo" arguments and returns a boolean.  Pish and tush -- that's
close to saying NOTHING about the known type constraints on P!!!

I'd like a language that just lets me state as little or as much as
I know and want to express unambiguously -- then the compiler
in turn can generate as little or as much static or dynamic typing
as it knows how to generate and/or it's directed to generate by
options or whatever, but meanwhile I HAVE expressed my design
intent in my sources -- *NOT* in possibly-ambiguous comments,
but in formal, unambiguous language that MAY, depending on the
state of compiler technology, turn out to help direct the compiler
to generate appropriate code.  I know of no language, except maybe
a few experimental ones (which I have not tried), which would let
me use quantifiers this way.

So, no language is even halfway good at letting me *express*
types, much less check such type-constraints "statically".  Might
as well use a language that doesn't *PRETEND* to support such
typing notions, no?-)


Alex