| ▲ | pvillano 4 hours ago | |
This stack exchange answer talks about the importance of decidability in type checking https://langdev.stackexchange.com/a/2072 My interpretation Decidability is of academic interest, and might be a hint if something is feasible. But there are (1) ways of sidestepping undecidability, e.g. A valid C++/Rust program is one for which the typechecker terminates in x steps without overflowing the stack And (2) things which are decidable, but physically impossible to calculate, e.g the last digit of the 10^10^10 th prime What matters is being able to reject all incorrect programs, and accept most human written valid programs | ||