Затестил Lean Theorem Prover, это бомба!

Lean Theorem Prover оказался лучше всех теорем-пруверов, которые я видел до сих пор, удобнее Coq, удобнее Agda (правда, это НЕ язык программирования, это только теорем-прувер). И главное, работает в браузере, не надо ставить всякую древнюю экзотику. И библиотека для гомотопического исчисления построений (HoTT with propositional resizing) сразу приложена. Раньше я экспериментировал с HoTT только на бумаге, неудобно работать было.

Правда синтаксические возможности послабее Агды, это увы. И TeXmode пока, вроде, нет.

maxim, а вот ещё интересно как оно в сравнении с TLA+ тулбоксом, я его не щупал пока.

Upd: Нету высших индуктивных типов, так что хрен я поиграюсь с тем, что интересно. Ну и взаимно индуктивно-рекурсивных семейств типов тоже ожидаемо нет, она вообще только в Агдачке есть. Охо хо. Нет пока щастья.

Кстати, хотел похвалить

Вчера звонил в хотлайн нашего провайдера Easybell рассказать им про траблу с интернетом. Мне с первого раза ответил человек, который не боится слов IP, DNS, "Прозрачный прокси" и "подсеть". Я был приятно удивлён, а проблему починили в течение часов трёх или четырёх. Не то чтобы прямо сразу, но вполне себе!

Из негатива: прозвониться в саппорт очень трудно, приходится висеть на линии и слушать нудную музыку минут по десять. Но зато сразу говоришь со специалистом, мне кажется это того стоит.