|
|
|
|
|
|
by UncleMeat
1143 days ago
|
|
|
Types can only decide trivial properties. But that's fine. We can accept false positives (valid programs that nevertheless type incorrectly and are rejected by the compiler). You still get very powerful reasoning with this. Dependent types are also equally stymied by Rice's Thm. Both are static techniques. Path based type reasoning doesn't do anything to solve the halting problem. It just means more expressive types. |
|
|