> I don't agree [#]. Providing a predicate that tests for identity of implementation enables a useful class of optimizations. For example, if you know two sets are implemented by the same object, you don't need to compare their contents to know they're equal. The fact that the information can be misused doesn't make it useless. Non-leakiness of abstractions isn't an unalloyed good.
You can have identity equality in Standard ML (resp. Haskell) too, it's just a matter of using the right types: a `foo` (resp. `Foo`) has structural equality, but a `foo ref` (resp. `IORef Foo`) has object identity equality. More precisely, equality is always structural, and identity equality is the right notion of structural equality for reference cells. So absolutely nothing is lost w.r.t. what you have in Lisp or Python. And you gain actual compound values.
> In practice, these are relatively minor. Consider for example my FSet collections library. One of the preconditions in the contract of each FSet operation is, of course, that the invariant required for correct operation holds on the object(s) on which the operation is invoked. Suppose we have proven, for each operation, that it correctly implements its contract: if the invariant holds on the argument(s), it holds on the return value.
Have you ever actually proving things about code? It's far from a “minor thing” when every operation has unchecked preconditions that you need to manually verify every time you call a function. The only reason why I can prove things about my code at a reasonable scale is that I arrange things so that I have to manually prove relatively little, and the rest automatically follows from type safety and parametricity.
> (next paragraph)
You use the word “probably” a lot. An argument that uses the word “probably” can't convince me that a proposition is true in all of the cases.
> I note that even your beloved SML doesn't mandate arbitrary-precision integers [1].
Hand-rolling big integers using machine integers as the starting point is easy in Standard ML. The final step is very important: Using abstract types, I hide the representation of big integers from the rest of the program. As far as clients care, they are using big integers, not lists of machine integers, vectors of machine integers, or whatever. Unfortunately, this final step is impossible to perform in Lisp.
> I can't even find, on its Web site, anything saying whether SML/NJ has them or not.
I don't use SML/NJ, because it has a lot of broken extensions that are difficult to reason about, and it uses a questionable external language to automate builds, rather than SML itself. Instead I use Poly/ML and Moscow ML. Both have big integers.
> Perhaps they are now considered a de facto requirement for a usable SML implementation -- in which case, you see, culture matters.
Big integers are great help, but they aren't considered a de facto requirement. The only requirements are those in the Definition of Standard ML and the Standard ML Basis Library. As I said above, using abstract types, you can roll your own non-leaky big integer abstraction.
> While language (mis)features do sometimes contribute to the difficulty of verification, most of that difficulty, I strongly suspect, comes from the complexity of the code itself.
And the complexity of the code itself comes from the discrepancy between your problem domain and what you can readily express in your programming language.
> We could verify machine language programs if we wanted to, and though it would be harder, I can't believe it would be overwhelmingly harder.
Well, you are overwhelmingly wrong, unless you hand-wave away a significant chunk of your proof obligation.