HOL Lightはなぜ挫折しやすいのか、その理由に正面から向き合うチュートリアル
HOL Light Tutorial
HOL Lightのマニュアルは詳細だが、面白いことをする前に大量の背景知識を吸収する必要があり、初心者には敷居が高い。そこで、段階的な例題を通じて基本的な使い方を素早く学べる「クイックスタート」ガイドが用意された。インストールからOCamlの基礎、論理、型、タクティクス、数論、実解析、プログラミング言語の意味論まで幅広く扱う。
HOL Lightの定理証明器は、使い始めるのがなかなか難しい。マニュアルはかなり詳細で包括的だが、ユーザーが何か面白いことをする前に吸収しなければならない背景情報の量は、威圧的である。