> Wow, this is even more broken than I previously thought.

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.

In fact, because all computations take time and space, no abstraction can be perfectly leak-free.

[#] Except if you want to make the point that the Lisp builtin function currently called 'eql' should have been called 'eq', and the function currently called 'eq' should have been called 'identical-objects-p' or some such long and explicit name. Formally this makes no difference, of course, but as a practical matter it makes erroneous usage of the latter much less likely and easier to spot.

> It causes difficulties when you want to reason rigorously about your code.

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.

So now we have an application, a complete program that uses FSet as a library. Among the many things we need to prove is that the preconditions of each FSet operation used in the application are satisfied. Because we've already proven that the FSet operations maintain the required invariant, we need to prove that nothing else in the program breaks that invariant. In a language with unbreakable access control, this would be trivial: no other code has access to the internals of these data structures. In Common Lisp, we have a little more work to do. We have to show that no other code invokes the FSet internal accessors by name; a few calls to 'grep' suffice for this. Then we have to show that there's no chance the code uses Lisp's reflective features to invoke these accessors indirectly: specifically, that no calls to 'intern' exist in the program that could return a symbol that names one of these accessors. This is probably easy. If the program calls 'intern' at all, it probably passes a constant string as the name of the package to intern into, so all we need to show is that that string is not equal to "FSET". If the package name is not constant, this starts to get a little harder, but (a) this is a rare case, and (b) if we can't easily prove that the possible package names come from a small, restricted set, the program probably has a security vulnerability and needs to be fixed anyway.

That's nonzero effort, I concede. But on the scale of all the things we have to do to verify our application, it's fairly trivial.

By way of contrast, let's look at what happens in languages where the default integer type has bounded precision. Now, to figure out the range of inputs over which some procedure satisfies its desired contract, we have to work backwards from each integer operation, looking at the range of values that would cause it to overflow, and figuring out what constraints that places on the inputs. This task can be quite difficult in complicated cases, and even in simple ones, the need to do it is easily overlooked (as shown by a famous example [0]).

I note that even your beloved SML doesn't mandate arbitrary-precision integers [1]. I can't even find, on its Web site, anything saying whether SML/NJ has them or not. Perhaps they are now considered a de facto requirement for a usable SML implementation -- in which case, you see, culture matters.

Look. Formal verifiability is a concern of mine too, and I understand where you're coming from. But this is not a black-and-white world, and practical considerations are also relevant. 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. 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.

[0] https://research.googleblog.com/2006/06/extra-extra-read-all...

[1] http://sml-family.org/Basis/integer.html