> (car a), a contains 42. Application bombs. That's an example of having the wrong tag, not type. > Not having the same tag in all executions isn't necessaril

> (car a), a contains 42. Application bombs. That's an example of having the wrong tag, not type. > Not having the same tag in all executions isn't necessarily an error, and the guarantee is not required. It being vanishingly improbable that there isn't a type error is good enough. A guarantee in this area has limited value; it doesn't anywhere near prove correctness. I absolutely agree that it isn't necessarily an error (though I do not agree on "good enough"; see below), but I was responding to your own assertion that the guarantee you got was just as good as what you got in a statically typed system, which it's not. Simple statically typed systems verify that the tag is the same by only allowing one tag, eliminating certain classes of error caused by trying to access data as though it were a particular type when it's not (at the cost of limiting the flexibility of your program); more complex ones allow multiple tags if desired, but require you to check to make sure that the tag is what you expect before going on to perform operations on the wrapped data. > I'm skeptical. An example program (Common Lisp, Ruby, Python, Scheme, ...) would be useful, which is fully exercised, via external inputs, such that no errors occur, yet more inputs can be found that trigger a slot-not-found type problem, or a wrongly typed value pulled from a slot. It's not that I don't think the program is possible, but that it has to be contrived. I don't care about catching fraud, only mistakes. It's really, really easy to do this. JSON parse a list of objects (your external input) that are expected to have the same shape. Then walk through the list, accessing a certain property (say, name). It is very easy to write a test of this that achieves 100% path coverage (harder if you need to count exercising every path of the JSON parser, but not material for the purposes of my point). It is also very easy to construct an input for which this will fail. It happens routinely when you store something in a json blob store or accept input over an API endpoint (I've seen it numerous times) so your skepticism that it can happen in real programs is unwarranted. If you want, I can write out a program that does it, but the description I just gave should suffice. Note that this can happen even if you carefully check to make sure that all input is of valid shapes and explicitly put them in structures (let's say you have three or four shapes that you consider valid in most lists). You can get a similar failure in a language like Java if you try to, e.g., downcast to a subtype of Object, while iterating through the list, without first checking what type it is (something I've seen people do not infrequently, occasionally with reassuring comments about how it can't fail; the comments are often wrong). Examples of array indexing failures with 100% path coverage is even easier, as should be evident from the numerous array-out-of-bounds errors that exist in C; the only difference is that they don't turn into buffer overflows in memory-safe languages, they're still there. Overall, I find your skepticism that bugs like this show up to be pretty unwarranted, especially since I work in dynamically typed languages every day, and my coworkers and I cause bugs like this in production pretty frequently, including in repositories with 100% code coverage.