Monthly Archives: October 2011

I’m not gonna write you a Coq proof

by ,

In NUS, I took CS3234, a Logic and Formal Systems course. The course instructors decided to use Coq, a theorem prover, to help us learn better. We used Coq to prove mathematical and logical theorems. For example, you could prove that the solution to the Towers of Hanoi is correct using mathematical induction in Coq. You could of course do it on paper but when the problems become tough, it’s much easier to use Coq.

Continue reading