This is just a tiny announcement. I’m going to start reading Software Foundations. I’ve heard great things about it, and I want to pick up a theorem prover in the process.
Here’s some sample Coq to start the adventure.
Inductive day : Type := | monday : day | tuesday : day | wednesday : day | thursday : day | friday : day | saturday : day | sunday : day. Definition next_weekday (d:day) : day := match d with | monday => tuesday | tuesday => wednesday | wednesday => thursday | thursday => friday | friday => monday | saturday => monday | sunday => monday end. Inductive bool : Type := | true : bool | false : bool. Definition negb (b:bool) : bool := match b with | true => false | false => true end. Definition andb (b1:bool) (b2:bool) : bool := match b1 with | true => b2 | false => false end. Definition orb (b1:bool) (b2:bool) : bool := match b1 with | false => b2 | true => true end. Example test_orb1: (orb true false) = true. Proof. reflexivity. Qed. Example test_orb2: (orb false false) = false. Proof. reflexivity. Qed. Example test_orb3: (orb false true) = true. Proof. reflexivity. Qed. Example test_orb4: (orb true true) = true. Proof. reflexivity. Qed.