alt Hacker NewsDecidability isn't even that useful. If typechecking takes a million years, that's also bad. What you want is guarantees that correct programs typecheck quickly. Without this, you end up in swift land, where you can write correct code that can't be typechecked quickly and the compiler has to choose between being slow or rejecting your code
> What you want is guarantees that correct programs typecheck quickly.
In practice there's wealth of lemmas provided to you within the inference environment in a way standard library functions are provided in conventional languages. Those act like a memoization cache for the purpose of proving your program's propositions. A compiler can also offer a flag to either proceed with ("trust me, it will infer in time") or reject the immediately undecidable stuff.