logic
2 free lessons tagged logic across Computer Science. Each one is a short sequence of focused steps with narration and a five-question quiz at the end — take them in any order, no signup required.
Types as Propositions: Making Wrong Programs Unwritable
The other tradition does not prove a program correct after writing it. It designs a type that only correct programs inhabit, so the compiler's ordinary check is the proof. This lesson builds the correspondence between types and logic, shows what dependent types add, and covers the price the approach charges.
What a Proof of Correctness Actually Is
Testing samples inputs; a proof covers all of them. The machinery is a logic in which programs are statements about how they change what is true. This lesson builds Hoare triples, works a proof by hand, and identifies the one step that cannot be automated and is therefore where the work is.