В опросе языков могущих в proof assistant(в основном это значит типы первого порядка) с большим отрывом побеждает Lean

Вот определение натуральных чисел на нем

inductive nat : Type
| zero : nat
| succ : nat → nat

def Nat.add : Nat → Nat → Nat
| n, Nat.zero   => n                      // n + 0 = n  
| n, Nat.succ m => Nat.succ (Nat.add n m) // n + succ(m) = succ(n + m)

логика тут в рекурсивности, шото вроде либо это 0 либо оно само + 1, получается если много делать succ то можно получить любое натуральное число, а сам факт того шо они натуральные следует из того шо тут нет вычитания

Главная цель когда делаешь в яп эксепшоны, сделать их оутпут минимальным и понятным
zero bullshit principle

тк кк игра в жизнь тьюринг полна, можно сделать игру в жизнь на игре в жизнь, а следовательно и фрактал на этом основанный
https://oimo.io/works/life/
и самое прикольное что ничто в таком фрактале не повтаряется ни в пространстве ни в времени

Пофиксил еще одну багу в лсп и осознал забавную вещь
Мне прям не нравится прогать в этом отвратительном изменчивом лайв-енвайроменте
И тут стоп, это же очень похоже на GUI, только компилятор
Ты не знаешь что и где сделает юзверь, и у него полно возможностей
Какой он файл откроет, в каком добавит новый тип, удалит функцию, при этом надо сохранять консистентной базу знаний о коде, получая только текст измененный юзвером

А еще оч запарно дебажить, дебажу принтами, и не обычными а специальными через апишку, если вывести чето на консоль то все взарветься, ведь в качестве шины обмена клиента сервера я использую инпут аутпут стрим

я очарован, можно это теперь будет моя ролевая модель при оценке задачъ?
https://youtu.be/jR6Si4e0m6U

^_^

В траве сидел #макмакич зелененьким он был
"Лучшее сочетание софта и железа" BTW,
дефолтный проводник которому 20 лет

От того факта что это возможно у меня появляются вопросы к апи плагинов IDEA

еще и на скале, я не удивлен https://github.com/axaluss/power-mode-intellij-plugin/tree/master