Research-led essays, new evidence, arguments, interviews and artifact studies from a history that is still compiling. Every seeded essay ships with inline citations and a Works Cited record.
Ed Catmull's 1974 graphics research mapped photographs and patterns onto curved surfaces, separating visual appearance from geometric complexity.
Bùi Tường Phong's normal interpolation and local reflection model let polygon meshes produce smooth shading and controllable specular highlights without changing their geometry.
Jack Bresenham transformed line drawing into an incremental integer decision process, giving plotters and raster displays an efficient way to approximate continuous geometry.
seL4 connected a high-performance microkernel implementation to a formal specification with machine-checked proofs, pushing software verification into the privileged operating-system core.
CompCert used Coq to prove semantic preservation across a realistic optimizing C compiler, closing the assurance gap between verified source programs and generated assembly.
Coq turned constructive type theory into an interactive proof environment where mathematical proofs become machine-checkable terms and verified programs can be extracted from formal developments.
TLA+ combines state-transition modeling, temporal logic and model checking so engineers can find concurrency and distributed-system design errors before implementation.
Z made abstract state, invariants and operations into a mathematical specification language, while Abrial's later B work pushed formal methods toward refinement and verified construction.
Model checking combined temporal logic with exhaustive state-space algorithms, allowing finite-state hardware and software designs to be checked automatically and failures returned as counterexamples.
Amir Pnueli brought temporal logic into program verification, giving concurrent and reactive systems a language for safety, liveness and behavior across time.
Dijkstra's weakest-precondition calculus turned program semantics into a backward calculation from desired postconditions toward the conditions needed for correct execution.
Hoare logic organized program proofs around preconditions, commands and postconditions, creating a compositional calculus that still shapes verification tools and software contracts.