Unsoundness is important because soundness and expressiveness come at a trade-off.
Here's some code which is syntactically legal in both TypeScript and Flow, but the languages disagree on whether a type error is present:
type T = { // Legal decl in Flow, illegal in TS
x: number;
[s: string]: boolean;
};
const m: T = { x: 1, xz: true };
m['xz'.substr(0, 1)] = true;
m.x.toFixed(); // Crashes
TypeScript is actually more sound than Flow in this example because it disallows the declaration of T in the first place. Flow allows this code and it fails due to a type error at runtime.
Yet in JavaScript this is an extremely common pattern - an object bag where some known property keys have a certain type, but "all the others" have a different type. You can't represent this in a bolt-on type system without forcing the developer to jump through enormous hoops proving that any lookup key isn't one of the "known" keys. By enforcing soundness at all costs, you lose the expressiveness needed to ergonomically describe this object.
Since most people don't directly aim guns at their feet, the unsoundness here is unimportant in practice. This is one place where I think Flow made the right trade-off to be unsound for the sake of practical usability for a common pattern.
Flow and its unsoundness is horrible. Quite often I can get runtime errors for code that compiled without warnings, and nothing for code that is showing warnings, because, amongst others, Flow's union type resolution is pretty abysmal.
Coming from Haskell, the level of unsoundness in Flow is very grating, and I would honestly not recommend it over untyped JavaScript... It luls you into a false sense of confidence that the program is correct, without it actually being so.
The problem lies in accepting "m['xz'.substr(0, 1)] = true;".
This line must only be accepted if a proof that 'xz'.substr(0, 1) != "x" is provided (for instance, inferred from a runtime check or encoded as a type) [obviously, that's impossible with that specific value]
While "unergonomic", code that doesn't do that is just broken and might for instance result in a security catastrophe if the key is attacker controlled.
"Will it be easy for a computer to prove that my API is being called correctly?" is not a question that JavaScript library authors seem to give any thought whatsoever to
That's generally not an option if the type in question is part of the interface of an external library. The type systems of Flow and TypeScript are both designed to allow typing of as much existing idiomatic Javascript code as possible.
Here's some code which is syntactically legal in both TypeScript and Flow, but the languages disagree on whether a type error is present:
TypeScript is actually more sound than Flow in this example because it disallows the declaration of T in the first place. Flow allows this code and it fails due to a type error at runtime.Yet in JavaScript this is an extremely common pattern - an object bag where some known property keys have a certain type, but "all the others" have a different type. You can't represent this in a bolt-on type system without forcing the developer to jump through enormous hoops proving that any lookup key isn't one of the "known" keys. By enforcing soundness at all costs, you lose the expressiveness needed to ergonomically describe this object.
Since most people don't directly aim guns at their feet, the unsoundness here is unimportant in practice. This is one place where I think Flow made the right trade-off to be unsound for the sake of practical usability for a common pattern.