not safe at all

[Tim Peters]

[Alex Martelli]
> ...
> 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!!!

LOL -- "pish and tush" is exactly on-target.

ABC (Python's predecessor) had quantified boolean expressions, of the forms

1.  each x in s has expression_involving_x
2.  no x in s has expression_involving_x
3.  some x in s has expression_involving_x

The keywords there are "each", "no", "some", "in" and "has".  They had a
very nice twist:  if an expression of form #1 was false, it left x bound to
"the first" counterexample (i.e., "the first" x in s that did not satisfy
the predicate expression); similarly if #2 was false, it left x bound to the
first witness (the first x in s that did satisfy the predicate); and if #3
was true, to the first witness.  For example,

    if some i in xrange(2, int(sqrt(n))+1) has n % i == 0:
        print n, "isn't prime -- it's divisible by", i

or

    assert no x in xrange(2, int(sqrt(n))+1) has n % i == 0, "n not prime"

According to Guido, Lambert Meertens (ABC's chief designer) spent a
sabbatical year in New York City working with some of the SETL people, and I
speculate that's where this cool little ABC subsystem came from.  I would
like it in Python too, but it's a lot of new keywords to support one
conceptual gimmick.  It's still a pleasant pseudo-code notation to use in
comments, though.

uncommonly-fond-of-constructs-that-capture-common-loops-ly y'rs  - tim