How are well specified contracts different from type script? Typescript is just annotation. Behavior cannot change. This is annotation plus runtime examinable behavior. This approach seems conducive to static checkers.

> How are well specified contracts different from type script?

Typescript has types, meaning expressions can be typechecked and this is distinct from evaluating them. Typechecking is more complete/consistent/reliable - you can catch type errors that don't show up in a codepath that gets actually executed. E.g. an empty list can be well typed, which as far as I can see you can't do with contracts.