3 ms·
In regards to the last paragraph. If the type system is turing complete, then the type-correctness of the program _may_ be dependent on the output of an arbitra
by seveneightn9ne 10y ago
In regards to the last paragraph. If the type system is turing complete, then the type-correctness of the program _may_ be dependent on the output of an arbitrary turing machine. Therefore, your type checker must be either incomplete or its result must depend on the output of the arbitrary turing machine.