jrh13/hol-light
View on GitHub ↗ ★ 569 OCaml
The HOL Light theorem prover
4 mentions on Hacker News by 4 people: 0 stories, 4 comments · first 2021-07-18 · latest 2026-08-05
20082026
-
…is a theorem. The HOL Light kernel (mentioned in the article) is about 500 lines from one file ( https://github.com/jrh13/hol-light/blob/master/fusion.ml ), and is a very straightforward implementation of a simple type theory (…
comment by momentoftop · 2026-08-05 · in Why is it all in the kernel? -
…provers are not part of the TCB. Here is an example of the TCB for an industrial strength prover: ○ https://github.com/jrh13/hol-light/blob/master/fusion.ml A mere 676 LoCs. This miniscule size of the TCB is where the comparatively lesser…
comment by GregarianChild · 2026-02-04 · in Broken Proofs and Broken Provers -
Thanks. There's also https://github.com/jrh13/hol-light which I think is still maintained (just learned about it in https://www.youtube.com/watch?v=uvMjgKcZDec from this thread: https://news.ycombinator.com/item?id=40619482 )
comment by dorfsmay · 2024-06-13 · in Terence Tao on proof checkers and AI programs -
…about subtypes is not really true. HOL Light has subtypes baked into the kernel of the system. See https://github.com/jrh13/hol-light/blob/master/fusion.ml lines 600-637. Coq has sig in the standard library which is not quite it but…
comment by cjfd · 2021-07-18 · in The metaphysical presuppositions of formal logic