mathematical theorems completely formally in higher order logic.
It sets a very exacting standard of correctness, but provides a number
of automated tools and pre-proved mathematical theorems (e.g. about
arithmetic, basic set theory and real analysis) to save the user work.
It is also fully programmable, so users can extend it with new theorems
and inference rules without compromising its soundness.
There are a number of versions of HOL, going back to Mike Gordon's work
in the early 80s. Compared with other HOL systems, HOL Light uses a much
simpler logical core and has little legacy code, giving the system a
simple and uncluttered feel. Despite its simplicity, it offers theorem
proving power comparable to, and in some areas greater than, other
versions of HOL, and has been used for some significant industrial-scale
verification applications.
