HOL Light

HOL Light is a lightweight implementation of classical higher-order logic developed by John Harrison in the 1990s. It is minimal in design — the entire logical kernel is approximately 400 lines of OCaml — yet it has been used for some of the most substantial formal verification projects in mathematics, including the Flyspeck project, which produced a formal proof of the Kepler conjecture (that the densest packing of spheres in three dimensions is the face-centered cubic packing).\n\nThe design philosophy of HOL Light is extreme parsimony. The trusted computing base — the code that must be correct for all proofs to be valid — is kept as small as possible. Every other feature, including the tactic system, the parser, and the user interface, is built on top of this kernel and is not trusted. If a bug exists in the tactics, it can produce an invalid proof, but the kernel will reject it. This separation between proof search and proof checking is the central architectural principle, and HOL Light implements it more ruthlessly than any other system.\n\nThe Kepler conjecture proof by Thomas Hales was originally a computer-assisted proof that used extensive numerical calculations. The Flyspeck project, carried out in HOL Light, formally verified that these calculations were correct, producing a proof that is entirely formal and machine-checked. The project took over a decade and involved hundreds of thousands of lines of proof script. It is one of the largest single formalization efforts ever completed.\n\nHOL Light is not a general-purpose programming environment like Coq or Lean. It is a theorem prover, pure and simple. Its OCaml implementation makes it extensible — users can write custom tactics and proof procedures in OCaml — but the object of study is always mathematics, not software. The tradeoff is deliberate: HOL Light sacrifices the Curry-Howard unification of programming and proving for a smaller, more auditable kernel.\n\nSee also: Higher-Order Logic, Isabelle, PVS, Formal Verification, Coq, Lean\n\n\n\n