That's pretty much what @pigworker is saying there too. I do find "execution is left to the reader" on the cheating side, though.
-
-
It's frankly ludicrous to object to the *typechecker*'s reluctance to run programs for ever. The legitimate comparison is the *runtime*.
-
Tongue firmly planted in my cheek there. Although I do wish typecheckers had a better grasp of the physical bounds of computation too.
-
Sure. And we'll get there. Totality is just the first step of expressing stronger promises.
End of conversation
New conversation -
Loading seems to be taking a while.
Twitter may be over capacity or experiencing a momentary hiccup. Try again or visit Twitter Status for more information.