Petros Papapanagiotou
Petros Papapanagiotou
No because it runs on the OCaml toplevel REPL and is not compiled.
Hate to say it, but that's a known problem. See [this paper](https://www.sciencedirect.com/science/article/pii/S157106611200028X) for a more detailed discussion and examples with worse consequences. Typing, in particular, is a common source of...
The [hol-info mailing list](https://sourceforge.net/projects/hol/lists/hol-info) is a good place to ask questions for HOL Light (among other HOL systems).
@brando90 HOL Light is not as popular or as actively developed as Coq. I guess it's a small community and we are all used to the (over 20 year old)...