Maybe you need graduality, sure. Plenty of systems (e.g. Typescript) have added a real type system that works gradually onto an existing system. While there are compromises to that approach, it's still a lot more effective than contracts IME.

▲

anon291 33 minutes ago | parent [-]

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.

	▲	lmm 20 minutes ago \| parent [-]
		> 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.