Ведь что мы хочем от искусственного идиота? Чтобы он не галлюцинировал, ибо как только он прекратит вести себя недетерминированно, белковое программирование сразу же умрёт :) Потому что в частности достаточно будет лёгких опенсорсных моделек.
Ведь что такое галлюцинация в коде? Это правдоподобный, но семантически неверный вывод. А сильная система типов кодирует спецификацию в типе. И уже есть к сож рабочие пайплайны вроде Lean + Copilot.
Так вот, сермяга которую я откопал, заключается в том, что (выразительная в частности) сила системы типов нам по большому счёту и нафиг не нужна, а нужна нам способность формулировать спецификацию в формальном виде и соответственно автоматически её проверять, ну и давать нейронке формальный фидбек в рамках строгой семантики, в которой она будет путаться существенно - 10...1000 раз - меньше.
(Пишу страшное, но HoTT это всё лишь ухудшает, и я даже молчу про экосистему.)
Европа Америка Китай сейчас прям очень мощно работают над proof-carrying code generation с обратной связью от тайпчекеров (ну или refinement types через SMT), ну а геопозиционно в России по-моему только я один тут ещё куда-то бреду :)
Хорошая новость однако, что в треке по гомотопической теории типов я инсайтом год назад добавил отдельный гайд Calculus of Constructions, ибо λC -- это топчик куба Барендрехта. Даю в гайде полную реализацию CoC на F#, по-моему буквально в 100 строк всё уместилось :)
Надо будет кстати ещё индуктивные типы к ним добавить до CIC, докрутить до агентов через DSL, и это будет победа
Там итоговый вывод я делал в пользу HoTT, ну вот кто ж знал что в эпоху ai-агентов именно завтипы внезапно окажутся топчиком при том что для них уже немало продакшн-реализаций. На "Функциональных архитектурах" всё это разберём.
ps. Пацаны5 норм, хотя и слишком сладенько закончились (подлизывание к цру, конгрессу...). За вечный шаблон американской мечты "свой магаз" и "грёбаный частный сектор" от президента, отдельный зачот :)
Хотя я думал, что будет ближе к классике "Люк, я твой отец".
upd. В ФА добавил материал, как можно и без завтипов в принципе обходиться на F# чисто через Хиндли-Милнера. Мили-машина защищена железобетонно от галлюцинаций нейронки!