|
|
|
|
|
|
by ufo
4446 days ago
|
|
|
The real way dependently typed languages dodge the undecidability problem is taht they "give up" on some valid programs. The output of the typechecker is either "proved the program is correct", "proved the program is incorrect" or "incondusive". If the result is "inconclusive" then it means that the programmer needs to manually provide a proof of correctness. |
|
|