[cbc] Correctness by Construction: Lecture today