The title of the class is “Programming Language” but the first thing we learn in class are proofs. Yes, mathematical rigourous proofs for such things as 1+1=2. And the language we are learning to write these proofs is Coq the formal proof assistant.

Still not clear on why we are learning proofs but from what the TA explained, we will be using Coq to proof and verify properties of programs and programming languages.

An example of a proof written using Coq

Theorem mult_0_plus : forall n m : nat,
  (0 + n) * m = n * m.
Proof.
  intros n m.
  rewrite -> plus_O_n.
  reflexivity.  Qed.

Coq is unlike any programming language I’ve learnt so far. As I’ve heard, Coq belongs to a category called functional programming languages which lets you use functions as though they were objects (?); perhaps something like function pointers in C/C++. Also, the functional programming style has no side effects ie. programs are purely functions which map input to output, exactly kind of like how mathematical functions are (mathematical functions do not care about the computational steps as long as mapping is the same).

So, until next time when I’m not so confused…