Type systems aren't magic. They do stop all incorrect programs from running, but also the majority of correct programs too.

anon291 5 hours ago | parent | next [-]

Luckily most everyday programs are typeable.

	▲	noosphr 2 hours ago \| parent [-]
		And you don't need cut in logic either: https://philpapers.org/rec/BOODEC It's just that your typeable program might take more data to store than there are bits in the universe. I'm not saying that types are bad. They aren't. I'm saying they aren't magic and they come with a trade off.

rerdavies 5 hours ago | parent | prev [-]

... for some spectactularly inconsistent and arbitrary definition of "correct program".

	▲	noosphr 2 hours ago \| parent [-]
		Yes, like giving the correct result for every possible input.