...Более того, у многих не получается создать что-то работающее даже просто в модели обмена сообщениями (база: изучайте akka, erlang, ну и формальную логику ↑↑↑ :)

...и более того, на моём ключевом практическом курсе трека объектно-ориентированного проектирования ребята-миддлы в итоге подчас запутываются даже в небольшом проекте на пару десятков абстрактных типов данных...

Признаю, это полностью моя недоработка 💯
как закончу второй курс по гомотопической теории, плотно прям берусь за доработку практики ООАП, забустим её моделью акторов Хьюитта.

HoTT же, думаю, останется навсегда лишь для самых умненьких (только 0,002% способны.... :).

=

Software/System Design -- это про то что вне зависимости от объёма вашего проекта у вас обязательно там и тут будут образовываться big balls of mud конкретно в вашем коде. И тут важно эксплицитно разделять три типа этого дерьма:

-- DevOps и System Design in Large: бесконечные архитектурные боли и страдания , связанные с интеграцией чужих каках (все эти опенсорсные либы, микросервисы брокеры балансировщики очереди куберы-шмуберы), подчас вообще чистый devops, который сегодня стало модным скидывать на чистых разработчиков;


-- System Design in Small: технические возможности кривейшие ограничения, накладываемые фреймворком, все эти MVC ORM...


-- Software Design/Programming in Large: наконец, собственно программный код, ключевая мякотка везде и всегда. Вы никуда не уйдёте от того, что в абсолютно любом крупном проекте обязательно будут сотни-тысячи сущностей, как их не обзывай (типы данных, классы, таблицы базы..), и вам придётся как-то увязывать (скорее всего асинхронную) логику их работы.

Я делал и буду делать акцент только на этом пункте, трек ООАП ровно про это. Девопсу и SD вас научат сегодня в любой подворотне, потому что это то что можно в проекте "пощупать", а вот PiL фактически нигде не найти (слишком абстрактно, примерно как рефакторинг для менеджеров).

Тут нужен действительно хороший практический пример, не учебный на 15 классов, а реально очень сложный именно в плане внутренней логики и нагрузки на процессор, и обязательно в реальном времени.

Склоняюсь к некоему учебному прототипу dwarf fortress (в тележке русский чатик очень живой)
Миллионы строк кода на плюсах, тысячи сущностей, и при этом уникальная сложность (глубокая симуляция физики, экономики, биологии ...)

Посмотрите легендарный тред " Dwarf Fortress source code":
the source code is so mind-buggeringly complicated and idiosyncratic that nobody else except Toady can really understand it

Тут ведь самое важное вот в чём: не запутаться в первых 16, 64, 256, 1024-классах, причём первые 2-3 шага ключевые. Хочу продемонстрировать вживую и, главное, "научать", как можно с самого начала и на всю перспективу удерживать линейной сложность программного кода с логикой взаимодействия тысяч типов сущностей в реальном времени даже для неоднозначного и нечёткого ТЗ с постоянными новыми хотелками.

И главное, чтобы это было доступно любому миддлу, этих ваших универов не заканчивавшего.

Дон Хуан из микрософта классный пост:

"Грядущая революция искусственного интеллекта в распределённых системах"

Как AI создал точные формальные спецификации TLA + из исходного кода Azure Storage, и затем выявил тонкий баг, который не сдавался классическим code review и тотальному тестированию.

Да, пока AI не так хорош в проектировании концептуальной системной архитектуры. Но дело в том, что большинство программистов также не так хороши в этом, а 98% уже значительно хуже AI.

AI постоянно галлюцинирует? Да вообще не имеет значения, что AI "не знает", что он делает, не понимает смысла создаваемого. В большинстве случаев мы сами тоже этого не знаем.

И с твоим проектом в итоге либо всё будет хорошо, либо нет. Одно из двух.

.

"Всё что нужно знать про Entity-Component-System"
(геймдев открывает для себя функциональное программирование:)

Ну, да, для системы с тысячами типов данных, как dwarf fortress, ECS + реляционная модель, "усиленная" джсонами.

Связи через графовые отношения:

Гном (id=123) держит меч (id=456) из обсидиана (id=789) =>
CREATE (:Сущность {id:123})-[:HOLD]->(:Сущность {id:456})-[:MADE_OF]->(:Материал {id:789});

Да вот только тривиальное "найти всех гномов в радиусе 10м, держащих деревянный меч", систему сразу подвесит :) Я бы ещё для хардкора DDD накинул, чтобы только первичные требования составлять пару лет (и через месяц реализации понять, что надо было делать совсем по другому).


-- Реактивщина + стрим процессинг?

Чисто лучше, да только помрёшь в отладке асинхронных цепочек событий )))
Поэтому и от модели акторов я наверное всё же откажусь.
"Возьми кафку", говорили они...


-- Онтика? RDF/OWL?

:Лава rdf:type :МагматическийМатериал ;
        :hasReaction [:with :Вода ; 
                      :produces :Пар, :Обсидиан] .
:Гном :можетДержать :Предмет .

+ SPARQL-ом "найти материалы, которые ржавеют при контакте с водой"

Пихаем всё графом в Neo4j...

да только оверхэд на инференс в реалтайме получаем уже на первых 50 сущностях :)

Разве что на Rust + Bevy пилить, да тут сам загнёшься соответственно от когнитивный перегрузки.

Родной df на плюсах, на райзене 5600 и так-то большой тормоз уже на паре сотен дварфов и сотне прирученных животных (и уж молчу про симуляцию магмы :)

-- На виртуально бесконечных ресурсах я бы выбрал скорее всего Event Sourcing + CQRS, тут не просто отладка элементарная, а мы вообще получаем по сути детерминированную машину времени, и решаем кучу проблем.

Собственно вот:
Domain-Driven Design: The Power of CQRS and Event Sourcing

Да только на практике в таком подходе заткнёмся ещё быстрее, чем с онтологиями...


-- На самом деле наиболее легко и просто было бы такое спроектировать просто в чистом ФП, да только из-за иммутабельности тоже совсем не потянет в плане продуктивности.

Размышления продолжаю.

Линзы кстати неплохая темка: когда мы фокусируемся на части структуры данных (своеобразная инкапсуляция геттеров и сеттеров в одной сущности).

Линзы неплохо обобщаются через профункторы: один интерфейс для разных операций; сложные операции выражаются через простую композицию "оптических элементов" (условно, как в гомоморфном шифровании).

А профункторная оптика, соответственно, расширяется до рефлексивной, и мы попадаем в мета-программирование.

-- Рефлексивное описание дварфа
dwarfSchema :: ReflectiveSchema
dwarfSchema = ReflectiveSchema
  { _fields = 
    [ ReflectiveField "name" stringLens [notEmpty] "Dwarf name"
    , ReflectiveField "health" healthLens [range 0 100] "Health points"
    , ReflectiveField "skills" skillsLens [validSkills] "Skill levels"
    ]
  , _relationships =
    [ Relationship "belongsTo" "fortress" fortressIdLens
    , Relationship "hasMany" "items" itemsLens
    ]
  }

-- Динамическое построение запросов
buildQuery :: String -> Query
buildQuery "dwarf.skills.mining > 10" = 
  Query $ dwarfSchema ^. field "skills" . field "mining" . filtered (> 10)

Оптику можно строить во время выполнения, генерация кода, конфигурируемые проекции.
Игрок может задавать собственные запросы... Но тоже нагрузочно конечно.

На хаскеле это всё красиво выглядит, но страшно далёк он от трудового итэ-народа.

Почему SaaS сегодня -- это проигрышная бизнес-модель?

Чтобы заключать крупные сделки, нужны корпоративные продажи (организовать такой процесс крайне тяжело), продвинутая техподдержка, постоянная кастомизация -- все те скучные и не требующие обслуживания вещи, с которыми так хорошо справляются Яндекс и Мэйл. Ещё в девяностые был случай, знакомой накодил опердень и ходил соло ставил по банкам триал на 60 дней. В одном банке триал закончился, а у них уже работа на нём ведётся, ему звонят "срочно!", он говорит "ну так надо же оплатить", после чего к нему приехали хмурые пацаны в кожаных куртках и сказали: финансовыми вопросами разбирайтесь сами, но банк должен сегодня заработать :)
Сегодня это впрочем стало цивилизованно: юристы просто придушат, и будешь по жизни поддерживать свой SaaS для таких забесплатно.

=

Если же будете ориентироваться на клиентов поменьше, то быстро поймёте, что SaaS -- это буквально гонка на выживание. Сегодная AI + low/no code развивается так быстро, что условный ООО/ИП 100500 раз подумает, стоит ли вкладывать в ваш продукт 10,000 рублей, вместо того чтобы за 2,000 рублей взять подписку на Клода 4, который сразу закодит 80% требований, или купить более дешёвый клон вашего продукта, который какой-то студентик запилил за 48 часов.

=

Cегодня у заказчиков-айтишников SaaS просто ещё считается "более настоящим" итэ-бизнесом, нежели условный "консалтинговый бизнес", но этот снобизм с развитием AI через годик полностью исчезнет.

Облако драгоценностей за неделю.

Основной паблик:

...Всего этого можно было избежать, если бы разработчики исходили из того, что любые их радужные предположения, скорее всего, неверны, а самым главным ошибочным из них будет представление о том, что всё будет идеально, ну или хотя бы "как и вчера".



Для донов-начинающих:

98% программистов, которые любили задавать вопросы про "полезненькое", заявляли "я хорошо обучаюсь", на практике входили где-то в топ-30% самых тупеньких...

Знания это не система.
Бессистемного опыта всегда недостаточно.
Искусственный интеллект не столько поможет, сколько заберёт или надолго заблокирует твои случайно нахватанные скиллы...


Для донов-неначинающих:

39. Жёсткий хейт SOLID | ISP (СильныеИдеи++)
Версия происхождения ISP такая, что дядюшка Боб много-много лет назад консультировал Xerox, и захейтил "God object" (это когда в один объект понапихали кучу всего), выступив в качестве Кэпа Очевидность. У них был некий божественный объект Job, и вот Мартин предложил просмотреть все места в коде, где он используется, для каждого такого места посмотреть, какая группа схожих методов там применяется, и выделить их в промежуточный интерфейс...

За 45 лет ИТ-карьеры я не видел НИ ОДНОГО программиста, кто [...] и при этом не имел бы профессиональных и финансовых результатов.


Напомню, что первые две дюжины существенно переработанных и улучшенных материалов СильныхИдей (по сути две книги) пока доступны на бусти, но дружелюбные цены уже начали расти:
1. БАЗА программной инженерии
2. Software Design с акцентом на Programming in Small


=

Новые материалы для курсантов.

В раздел "Элитный программист" добавлен материал
67) Лучший хак продуктивности.
Мы часто перегружаем свой день, пытаясь быть продуктивными и сделать больше дел. Вместо этого тебе надо ...

=

Курс "Гомотопическая теория типов для программистов (2)": этим летом курс 💯 будет готов.
Закончил универсумы (формальное понятие типа, иерархии, полиморфизм и произведение универсумов, пространство функций...).
Всё это детально разбираем на питоне, и останется домоделировать унивалентность и эквивалентность типов. Потом добавлю кубическую теорию третьим курсом. По увлекательности и глубине с этими темками никакие шахматы или паззлы вроде baba is you и близко не сравнятся.

И понемногу улучшаю трек "Ясное проектирование", как делать системы с логикой уровня dwarf fortress, на тысячи типов/классов/таблиц так, чтобы сохранять сложность линейной. Я кстати придумал таки, как с этим всем быть и, главное, как этому наиболее продуктивно обучать, но узнают это уже только мои курсанты.

В частности, спустя четыре года вернулся к курсу "Ясная архитектура" — потому что сегодня для программистов владение архитектурными стилями становится едва ли не важнее, нежели само программирование!
На том курсе мы разбираем 13 "клиент-серверных" стилей на практике, с работающим кодом, от хипстерской говноархитектуры, классической процедурщины и объектщины, далее функциональная архитектура, Functional Core / Imperative Shell, Stateless-архитектура (как правильно избавляться от мутабельности), обычный DI, два вида функциональной инъекции, очереди на десятки тысяч rps, архитектура на монадах состояний и т.д.
Добавлю ещё штук пять стилей, включая упоминавшиеся, этим летом 💯

Сегодня прекрасный, Духов день 🙏 (всегда бывает дождик, кстати)!

Батюшки по всей Москве изгоняют AI-бесов из уличных роботов 👊

Мне приснилось, как я лечу в небе высоко в облаках, как Гум-Гам 😇

Кстати очень рекомендую, прочитайте своим детишкам эту светлую фантастическую повесть из 1970-го, советского святого писателя Евгения Велтистова (сперва книга, потом фильм): пророческое, как AI АВТУК порабощал людей.

(сегодня буду много постов размышлять текстом, важная тема, потерпите пожалуйста 🙏🙏🙏)

Сейчас тренд на всё своё "доморощенное" (в целом совершенно правильный, без иронии, я ещё с 90-х компьютерным журналистом в PC Week/RE написал сотни статей ровно о важности "национального" в ИТ, и свои взгляды никогда не менял, но тогда такие идеи были совершенно не в тренде). И вот наконец дождался, прошло всего-то 30 лет.

"свой ОС" "свой геймдев движок" "свой смартфон" "свой мессенджер" "свой проц" "свой приставка" "свой AI"...

Даже появилась "свой IDE" (где в about приведена ссылка на лицензию it-компании, которая демонстративно донатит врагам).

Хотя странно рассуждать о полноценном развитии "своего итэ", если оно не происходит прежде всего на базе своих фундаментальных разработок. Например, интел однажды слил полмиллиарда долларов из-за неверного проектирования чипа, и теперь активно применяет для этого всяческие системы верификации, включая SAT/SMT-солверы (формальные решатели). Как думаете, наши СБИС на каком софте проектируются, и насколько теперь ему можно доверять? А сегодня доля верификации в бюджетах таких проектов -- до 70% затрат на разработку СБИС.
Кстати, и рынок верификации смарт-контрактов с нынешних $300 млн. к 2030-му вырастет примерно в 7 раз, а у нас цифровой рубль, планируется крипту разрешить...

Но конечно никакого даже "свой солвер" нету и помине; в Стеклова и универах пользуют только зарубежные, вроде микрософтовского Z3 с кучей закладок для РФ.
Например, лекция микро-курс по SAT/SMT делал в МГУ приглашённый индус Vijay Ganesh. Хотя, по большому счёту, это уровень дипломного проекта, ну максимум аспирантского.

И уж тем более по формализации математики пустота. Филдсовский лауреат Tao вон буквально упарывается в обучении математиков современным it, и ключевой акцент, конечно, на proof assistant-ах и языках с завтипами: Coq, Lean, Agda, Isabelle, F*, Idris...

Coq ведь начинался усилиями советского математика Владимира Воеводского (гомотопическая теория типов), и посмотрите, что он сегодня представляет после ребрендинга: Rocq Prover. Вся академическая Европа и США сидит в основном на нём, и нам по определению на это теперь путь заказан.

Риторическое: надо ли делать "свой солвер", "свой пруф-ассистант", "свой формальный верификация"? При том, что последние топовые математики в этих темах уехали в европы...

Я кстати послезавтра Школу закрываю, серьёзно. Уже начались гонения штрафы онлайн-школ, кто без образовательной лицензии работает; принципиально не буду получать. В Индии например государство только поддерживает энтузиастов айти-обучения...

...Так-то мне это просто сильно интересно, поэтому в любом случае продолжу впроголодь развивать парадигму топологически-ориентированного программирования на базе гомотопической теории типов. Мой подход пока хотя и учебный, но чисто технически/архитектурно потенциал его несравненно выше существующих пруф-ассистантов и теорем-пруверов, потому что они сами по себе фактически полузакрытые фреймворки, где требуется огромное количество ручного ввода, а интеграция с чем-то внешним серьёзно затруднена. Верификация кода на 5,000 строк требует 200,000 строк кода доказательств :)

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

Стратегически в планах сделать (причём именно в таком порядке)
1 "свой формальный верификация"
2 "свой пруф-ассистант"
3 "свой солвер"

Солвер же это на сегодня задача по сути чисто техническая, никаких питонов, сразу надо делать скоростную версию на rust. Но там такая логика, что для реальных проектов нужна оперативка на сотни гигов, для возни с булевыми формулами. Никогда уже не накоплю на раб.станцию, на последние гроши взял свежую книжечку "Введение в алгебраическую топологию" (лекции на мехмате МГУ, в Новосибе: симплициальные, сингулярные и клеточные гомологии, связь с гомотопическими группами клеточных пространств, кольцо когомологий, двойственность Пуанкаре...). Не исключено, что сильная математическая база вполне может снять кучу технических проблем.

Почему я у всех этих западных пруверов-шмуверов (далее - Эти) потенциально выигрываю архитектурно? И насколько вообще мои оценки адекватны?

Ну, сегодня к счастью есть достаточно объективные AI-консультанты, шарящие в математике весьма уверенно (вдобавок, напомню, математика существенно проще чем программирование). Я спрашивал и у клода+опуса 4, и у гемини 2.5, и у дипсика и квена с дипсинками, показывал им свой код, и получил очень позитивный фидбэк. Основные претензии чисто у вас недоделано вот тут, а технически не хватает вот этого и того, ну дык, это уже дело времени. Реально очень доволен, даже сам не ожидал 🙏

Потому что всё Это ихнее делалось с нуля, вообще без опыта подобных проектов, а внутри, может их гитхабы посмотреть, это тотальное говнолегаси, которое писали не программисты-архитекторы с многолетним опытом, а преимущественно математики, да ещё и подчас на хаскелях! 🫢

Coq (индуктивные типы и тактики), Isabelle/HOL, Lean основаны на "классических" теориях типов или логике высшего порядка, и вполне обходятся без унивалентности (самая мякотка гомотопической теории). Унивалентность позволяет рассматривать равенство как эквивалентность (изоморфизм) между объектами, что крайне полезно при проверке соответствия интерфейсов или в модел-чекинге.

Я только-только вчера добавил транспорты между путями в ТОП: автоматическое перемещение между "равными" объектами без необходимости явного (ручного) доказательства инвариантов. А у Этих требуется доказывать корректность программ относительно их спецификаций через явные отношения между объектами (изоморфизмы, биекции...), писать крайне громоздкие конструкции для выражения эквивалентности (аксиомы выбора, дополнительные предикаты...). А я потенциально могу работать вообще со "структурами до изоморфизма" (например, в теоркате, при верификации распределённых систем, c гомотопическими типами...).

Кроме того, дальше вообще без проблем добавить "кубики" (чтобы строить модели в конструктивной метатеории, через конструктивную интерпретацию равенства эквивалентных типов), а этот ваш Lean 4 вообще на такое не способен, ну или через кривые приляпки, потому что его реализация использует UIP (Uniqueness of Identity Proofs), что противоречит принципам HoTT, где равенства -- это пути в гомотопическом пространстве (+ кубическая теория позволяет манипулировать "равенствами" напрямую, через операции и композицию 💪🏻 ).

-- Сергей Игоревич, но ведь можно и без HoTT доказать соответствие реализации спецификации?

Конечно, и это успешно делается десятилетиями (за многие миллионы долларов :)
Так или иначе, классические основания покрывают >95% задач верификации ПО, включая верификации микропроцессоров или криптопротоколов.

То есть и без HoTT вполне можно доказать полноценную корректность системы. Практически все крупные успешные проекты верификации (коих можно пересчитать по пальцам одной руки :) были выполнены без HoTT, используя классические основания:
- теория множеств (ZFC) в математических доказательствах;
- интуиционистская/логика высшего порядка (HOL) в Isabelle;
- исчисление конструкций (CoC) в Coq/Rocq/Lean.

В CompCert (верифицированный компилятор Си на Coq) корректность доказана относительно формальной семантики Си и ассемблера, без использования унивалентности. В ядре seL4 (Линукс по заказу АНБ) с помощью Isabelle через классическую реляционную семантику гарантированы изоляция процессов и сохранение инвариантов.

Когда же HoTT рвёт все Это как тузик?
1) Когда спецификация содержит гомотопически-инвариантные требования (топология, геометрия, перенос структур между изоморфными представлениями). Например, в классических системах (даже с зависимыми типами!) изоморфные структуры формально различны. А в HoTT унивалентность автоматически отождествляет эквивалентные типы, а транспорт вдоль путей позволяет легко и просто переносить доказательства между ними (всё это подробно разбираю для курсантов).

2) Когда становится технически очевидными ограничения Этих систем -- а таких ограничений сегодня множество, и чем дальше, тем больше, от медленной работы самих программ в реальных задачах до огромных объёмов ручной работы для доказательств эквивалентностей. А перейти с них на HoTT тоже сильно тяжело по самым разным причинам (математика HoTT требует переобучения -- например, по замене равенства на гомотопии).

Другими словами всё Это современное (а на самом деле уже давно легаси и big ball of mud) -- как ньютоновская физика, работающая в весьма ограниченных рамках, а HoTT - как математически обобщённая ТО.

(заключительное и спасибо за внимание; всё додумал с вашей помощью ❤️❤️❤️)

Насколько это всё серьёзно?

Навскидку, это прежде всего военные и аэрокосмические контракты, типа "Formal program verification in avionics certification"
Five years after the official adoption of the new DO-178C/ED-12C standard and its supplements, including the DO-333/ED-216 supplement on formal methods, no avionics-certification project has yet acknowledged using this new supplement. However, formal method technologies do exist that would ease the development of avionics software.

У них там преимущественно, формально верифицируется Язык Ада :)

Суммы? Georgia Tech Applied Research Corporation, Atlanta, Georgia, was awarded a $8,051,218 cost-plus-fixed-fee task order for development of a software-based system certification tool. Air Force Research Laboratory, Eglin Air Force Base, Florida, is the contracting activity

Думаете, у нас хотя бы 8 млн рублей МИАН Стеклова на подобное получил? Фиг.

Шикарный свежий обзор темки от индуса:
evolution-formal-verification-from-theory-to-industry (впн)

Короче говоря, я буду следовать роадмапу, который предлагает Центр технической информации Пентагона в своём контракте с Карнеги-Меллоном "Formal Verification of Mathematics in HoTT-Lean" (впн)

This project was used to support the research group in Formalization of Mathematics in the Homotopy Type Theory system, implemented in the Lean proof assistant at Carnegie Mellon University... Using this breakthrough, new computer systems are being developed for the formal verification of mathematical theorems and critical computer software.

(на лине делают, ха-ха, дурачки, стратегическая ошибка 😎 лин4 с 3м несовместим, и от хотт отказался)

И в заключение остаётся взять какую-то тестовую, но достаточно показательную задачу, по которой можно было бы сравнивать простоту и производительность моей реализации со всеми Этими. Далеко ходить не надо:

The value of the 5-state winning busy beaver was discovered by Heiner Marxen and Jürgen Buntrock in 1989, but only proved to be the winning fifth busy beaver — stylized as BB(5) — in 2024 using a proof in Rocq.

Вот для наглядности и реализую задачку поиска и конструирования Усердных Бобров (что это??) с 2-3-4-5 состояниями, и сравним (для шести состояний так-то надо 2,5 ⋅ 10^2879 шагов).

В тему: "Ехали тьюрмиты и тримувьи на машите Тьюринга"

Сегодня Будда ушёл в нирвану, так же исчезает и моя Школа...

Никакого учения и обучения у меня больше нету.

Всём спасибо, всех обнял.

❤️❤️❤️❤️❤️

Минобр вот-вот разрешит студентам-инженерам (без лицензии 007) учить в школах математике и физике (и это очень правильно). Любой чел сегодня может написать книгу "Учебник Django для лохов" или "Учебный курс просветления за 15 минут" и получать авторский гонорар от издательства за свои образовательные рекомендации.

И в то же время если вы например учительница и подрабатывайте репетиторством, или консультируете как вкусно заваривать кофе, или платно учите как делать классные мемы с помощью AI, или продаёте видеоролики, как на звезде мотоцикла запилить зубья болгаркой -- сегодня вам вполне может прилететь штраф на полмиллиона рублей (и уже появились первые прецеденты), а с 1 июня 2025 и присесть можно на "пятёрочку" -- не за финансовые/налоговые махинации, а конкретно за ведение образовательной деятельности без лицензии.

Бизнес в России развивать легко и просто, говорили они...

Graviora manent.

Игрок, понявший, что заведение жульничает всегда, встает из-за стола.
Рано или поздно в человеческом мире остаются только тупо заблуждающиеся особи, подверженные самому убогому гипнозу. И не просто подверженные, а с радостью готовые передавать гипноз дальше...
Виктор Пелевин, "Смотритель"

Но так-то, дорогие пилигримы, конечно же я всё равно продолжу учить правильным вещам в итэ, освобождая обречённых на глупость из океана программистской сансары 😇

🔥 за свои убеждения (образование должно быть свободным!) готов сгореть на костре 🔥

Чисто косметически, сперва надо сделать "ребрендинг", думал например над вариантами

Fakультативные Zанятия c Bобровским S.
Научный Фонд Сергея Бобровского
etc

Пока решил остановиться на этом:

🇷🇺 Лаборатория Математики и Программирования Сергея Бобровского 🇷🇺
(ЛаМПовое с Бобровским)

Формальное позиционирование ЛаМПы теперь такое, что это будет секта я просто предлагаю всяческие полезные материалы и книги, никакие не учебные, не обучающие и не образовательные, чисто справочные 🤓

И соответственно надо будет выполнить постепенный "рефакторинг" всего контента: вместо курсов и проектов -- гойды гайды, исследования и эксперименты, вместо курсантов -- верволки послушники пилигримы программирования, и т.п.

Посвящение в гомотопическую теорию типов отразится на глубочайших слоях вашего подсознания. Поэтому вам будут поручаться особые дела. Находящиеся на грани здравого смысла. Мистические. Неразрешимые.
"Круть" Пелевин-стайл)

А я буду за вас молиться 🙏

p.s. Нашим гимном будет "Экспериментатор".

Поставил MAX, на уже совсем ближайшее грядущее будущее (хорошо ещё что не баклажан на фоне; что это вообще за масонская символика? :).

Закончил второй гайд "гомотопической теории типов для программистов", осталось на сервер выложить и потестить, в заключение добавил хардкорные тесты, думал не прокатят, но сработало, даже сам удивился 🤘

и дальше будет третий гайд "кубики" - кубическая теория типов, по заветам военных заказов Пентагона
"...extending the original foundational system of Homotopy Type Theory by enhancements based on cubical methods from algebraic topoology in order to make the resulting system more algebraic, and thus more computationally tractable".

В качестве примера думал сделать например абсолютно защищённый + формальный верифицированный мессенджер, в тему зачитался, смешное
"История о том как абсолютное оружие оказалось никому не нужным"

Тут только есть крохотный нюансик, что едва попробуешь на базе такого мессенджера строить хотя бы малейшие коммерческие сервисы - например консультационные, рекламные, учебные , как по пост.313 тут же окажешься виновным по ст.171 😁

Очередное разочарование и избавление от иллюзий (и это очень хорошо): оказывается, когда нам говорят "ну вот же, вот, посмотрите -- математики это доказали, вот статьи в авторитетных журналах" - в 99,98% случаев это никакие не доказательства - в смысле конструктивных подходов - потому что для этого требуется отдельно доказать, что придуманное кем-то там доказательство верное. Сейчас такое доказательство доказательства единственное: мнение экспертного сообщества, и тут политики всё больше и больше.

Причём сами математики не шибко-то стремятся использовать современные теорем-пруверы - потому что если таким образом формально попроверять их работы, то весьма вероятно oкажется, что многие из них отнюдь не настолько "доказаны", как считалось. А за такие работы платят весьма прилично.

Хороший пример -- разрекламированная по всему миру шумиха вокруг якобы решённой проблемы BB(5) про Усердных Бобров -- дескать, математики не только это доказали, но и формально верифицировали сам процесс доказательства!

Сайт проекта bbchallenge , их спонсоры prgm.dev , код бобров на github.

Да, но...

"Природа, вероятно, встроила в машины с пятью состояниями одну или несколько проблем, столь же иллюзорных, как гипотеза Гольдбаха. Или, другими словами, скорее всего, будут существовать безостановочные рекурсивные паттерны, которые мы не в состоянии распознать."
Аллен Брэди, BB(4)

Так вот оказывается, что если копнуть чуть-чуть поглубже, то выясняется что это всё — огромный фейк ☠️

Сперва надо было классифицировать все 63,403,380,965,376 возможных 5-состояний машин Тьюринга. Затем надо было сам алгоритм моделирования машины Тьюринга запустить, соответственно, 63+ триллиона раз, применить эвристики быстрой классификации, и отобрать кандидаты с максимальными значениями.

Так вот сермяга в том, что 99.9% бобров классифицируются быстрыми эвристиками, а отнюдь не формально верифицированными доказательствами.

В чём же тогда заключается "доказательство" BB(5)?

"Решение" BB(5) = 47,176,870 основано на:
✓ формально верифицированных алгоритмах (~1% работы)
? эвристиках быстрой классификации (~98% работы)

Да, но отсутствие багов в коде? Корректность аппаратуры? Корректность самих эвристик? Нет, конечно.

Полностью верифицированные формальные доказательства строились на Coq только для самых трудных единичных случаев (особенно для доказательства незавершимости). Например с огромным трудом удалось доказать (или опровергнуть), что самый проблемный бобёр (1RB 1LC 1RC 1RD 1LA 1LA 1RB 1RH 0LE 1LB) никогда не достигает состояния HALT.

Корректность реализации симулятора, что он корректно выполняет переходы (так-то это 15 строк на питоне, разберём их верификацию в моём гайде:), доказывалось на Isabelle.

Алгоритмы обнаружения циклов и квази-поведения формально верифицировались на Lean.

Ну и всё. Всё остальное 98% — чистая программная инженерия.

Эвристика: "Машина зациклилась после 1000 шагов"
Реальность: Машина остановится через 10^100 шагов
Результат: Пропустили рекордсмена! 🙈

=

Короче говоря единственное что можно сказать — это чисто инженерное решение с некоторыми математическими гарантиями.

— BB(5) ≥ 47,176,870 (это точно доказано)
— Существует 5-машина, которая производит именно 47,176,870 единиц.

И не более. Конечно, на 99,98% скорее всего именно так и есть — и всё же...

=

Требуемое моделирование с множеством эвристик – это не недостаток методов, а неизбежное следствие природы вычислений. Из-за фундаментальных теорем неразрешимости (Райс, проблема останова) это области, где интеллектуальный перебор, глубокий анализ конкретных случаев и изобретательные эвристики — единственный практический путь вперёд 💪🏻

Достижения в вычислении BB(5) и начавшиеся атаки на BB(6) — это триумф человеческой изобретательности в преодолении принципиальных математических барьеров 🚀

А зачем вообще люди занимаются этим, насколько это подобное вообще "серьёзно" ?
Ну, не более серьезно, чем 98% всей теоретической математики :)

Чем выраженнее ваше мотивация по созданию стартапа "(тупо) заработать денег", тем сильнее вероятность вашего успеха стремится к нулю.

Соответственно, если вы создаёте стартап только ради денег, то вероятность того, что у вас ничего не получится, равна 💯

Под стартапом я имею в виду в принципе и "сделать враппер для жпт", и "склонировать топовую игру под андроид, заработавшую много бабла, чтобы повторить её успех хотя бы на 10%", и "хочу войти в айти за хорошую зарплату и соцстатус, в нашей деревне это единственный социальный лифт" и т.п.

Дальше дам БАЗУ для тех, у кого есть мотивация на 98% просто делать что-то полезное для других, и на 2% чтобы это дело приносило адекватные деньги.

С чего начать с полного нуля, если вообще не знаете и не представляете, каким должен быть самый первый шаг.