HOL Light обзавёлся учебником для быстрого старта
HOL Light Tutorial
Официальное руководство по HOL Light отпугивает новичков объёмом фоновых знаний. Новый туториал предлагает альтернативный подход: пошаговые примеры от установки OCaml до формализации теорем, включая RSA, анализ и даже парадокс Кохена-Спекера. Материал учит основам работы с системой на практике, не требуя предварительного чтения сотен страниц мануала.
HOL Light может быть довольно сложно освоить с нуля. Хотя руководство достаточно подробное и полное, объём фоновой информации, который нужно усвоить, прежде чем пользователь сможет сделать что-то интересное, пугает.