re: Types as propositions, programs as proofs VIEW POST

TOP OF THREAD FULL DISCUSSION
re: There are proof checkers. I'm not familiar with them though. I believe Coq does something similar. Could you do this for an interpreted language?...
 

Agda and Coq are both languages that also forbid infinite loops and thus have type systems that allow you to prove logical statements (via the Curry-Howard correspondence) about your programs.

It is cool to know your program has certain properties for all inputs by proving it, but also very time consuming :)

code of conduct - report abuse