HOL Light is a system to produce formal proofs. Most of what I know now came from the paper Formal Proof by Thomas Hales. It is the best introduction I have seen to HOL and it describes the history of machine checked proofs. Much of the recent history he reports was new to me.

Indeed I was sufficiently impressed with HOL that I decided to try it out. The experience has been sobering so far (Nov 2008). HOL is written in Ocaml, which is a language I am acquainted with. (I am acquainted with the language, not the mechanism of compiling Ocaml programs to run on my Mac.) Installation of HOL requires that Ocaml be on your machine. It further requires a program called camlp5 which is another OCaml program which works somehow with the Ocaml system in order to support a modification to the OCaml language syntax.

To run an Ocaml program it suffices to run the install package from Inria. To compile Ocaml programs requires learning extra steps. I have not found out what makes Ocaml pay attention to camlp5 in order to achieve a compiler that knows the new syntax. The HOL installation instructions are written in the new syntax and the corresponding semantics is guessable.

The Ocaml site claims that X11 is required to run Ocaml. (That is not so for I have run many Ocaml programs on my Mac in the interactive mode. Perhaps X11 is necessary to compile them.) My X11 reflexes have atrophied since I last used X11 briefly on Solaris 10 years ago. The documentation that I have found for X11 on the Mac assumes a user with acute Unix X11 reflexes and the documentation for X11 on Unix is bulky. When I did use X11 I relied on the kindness of strangers.

In short, HOL is far from being a Mac program.