Will Crichton

Dart - covariant subtyping of arrays is unsound, but convenient and can be caught at runtime, iirc

Great example. The point being that this is allowed, right? f : Array<Object> -> ... Array<int> a = ... f(a) // type checks Array<Object> b = a; b.push("string") // type checks & runtime error

Does TypeScript count? https://www.typescriptlang.org/docs/handbook/type-compatibility.html … says things like "The places where TypeScript allows unsound behavior were carefully considered", which sounds like what you're looking for.

It does, although I'm realizing "sound" is hard to characterize. In a PLT sense, Typescript statics + dynamics are collectively sound b/c anything not caught by type system is checked at runtime. No stuck states / UB / segfaults / etc.https://twitter.com/wcrichton/status/1285700061712785408 …

TypeScript: https://www.typescriptlang.org/docs/handbook/type-compatibility.html#a-note-on-soundness …

Eiffel, somewhat infamously, intentionally allows unsound method calls.

Sorry, to be more precise, Eiffel alows a subclass to override a method with a method whose parameters have types that are subtypes of the parameter types of the base method.

Wouldn't explicit UB in any ISO language (C, C++, etc) count?

It does, although I've never been 100% clear on how intentional it is. I know of claims that it's necessary for compiler optimizations, but I haven't seen any arguments as to why.