|
|
|
|
|
|
by mafribe
4023 days ago
|
|
|
I agree that it is good separate programming and verification. Otherwise the programmer is forced by the compiler to
worry about correctness and termination from Day 1. Moreover, Cury-Howard based approaches really work only for a
restricted form of programming: pure and total functions. |
|
|