HOL Light es un demostrador de teoremas que puede resultar intimidante para principiantes debido a la complejidad de su manual estándar. Este documento ofrece una guía alternativa de inicio rápido, diseñada para enseñar el uso básico mediante ejemplos graduados y simplificar el proceso de instalación en entornos modernos. El sistema está construido sobre el lenguaje de programación funcional Objective CAML (OCaml) y requiere su instalación previa como requisito fundamental.
La instalación varía según el sistema operativo. Para usuarios de Windows 10 o superior, se recomienda instalar Windows Subsystem for Linux (WSL) para acceder a un entorno Unix-like, o utilizar Cygwin como alternativa compatible. En Linux, la instalación puede realizarse mediante gestores de paquetes como OPAM, apt-get (en Debian) o directamente desde el repositorio de GitHub. Se detalla el proceso de clonación del código fuente, la compilación de las librerías de OCaml necesarias y la configuración del entorno de desarrollo. Una vez instalado, el usuario puede iniciar una sesión interactiva con el comando ./hol.sh, lo que permite probar el sistema y utilizar editores de código como Visual Studio Code con el plugin específico de HOL Light. Esta guía busca reducir la barrera de entrada para quienes desean explorar la verificación formal de teoremas sin necesidad de dominar todos los detalles técnicos del manual original.