Isabelle/HOL: первые шаги Если коротко, Isabelle/HOL - это среда для формальных доказательств, где математика жестко доминирует на кодом. Как начать: 1)Скачиваем с isabelle.in.tum.de 2)Запускаем jEdit, да у изабельки своя собственная IDE 3)Создаём файл с расширением .thy (например, Hello.thy) theory Hello imports Main begin end Имя теории должно совпадать с именем файла. imports Main всегда нужен - он подключает стандартную библиотеку HOL, в которой уже реализована и доказана вся школьная и университетская алгебра. Константы и функции Константа: definition x :: nat where "x = 5" value "x + 2" вернёт 7 Функция (рекурсия тоже работает): fun double :: "nat ⇒ nat" where "double n = n + n Isabelle сам проверит типы и что рекурсия корректна. Если что-то не так - отметит место с ошибкой. Типы данных: nat - натуральные числа (0, Suc 0, Suc (Suc 0) …) int - целые (включая отрицательные) bool - True / False string - строки (по сути, списки символов) Примеры: value "if (2 < (5::nat)) then 1 else 0" вернёт 1 value ""foo" @ "bar"" вернёт "foobar" Доказательства, леммы, свёртки, лямбды рассмотрим в следующих постах серии, там все намного сложнее и интереснее, чем просто в объявлении переменных и функций.