Наконец, ProVerif: символьный подход к анализу протоколов, аналогично Tamarin, но с акцентом на автоматизированное рассуждение о криптографических свойствах. База -- типизированное расширение пи-исчисления с криптографией, язык моделирования параллельных процессов...
Криптографические примитивы (шифрование, хэширование, подписи) моделируются через функции и уравнения. Символьная модель криптографии Долева-Яо, клаузы Хорна (привет, Пролог), по сути абстрактные методы анализа, которые авторы сами придумали:)
Сложные структуры данных (например, вложенные списки или рекурсивные типы) требуют ручного моделирования.
=> ProVerif будет более практичным -- для автоматического анализа криптографических протоколов в символической модели.
В HoTT же например, можно определить тип "протокол с условиями на последовательность шагов", которые автоматически проверяются системой, и так можно верифицировать протоколы с жёсткими структурными ограничениями,
HoTT интегрирует категориальную логику и теорию гомотопий -- мощные математические инструменты для доказательства свойств безопасности, что особенно полезно для анализа протоколов с распределённой логикой или сложными взаимодействиями (можно например формализовать, что протокол удовлетворяет условию инъективной эквивалентности.)
В общем, HoTT превосходит и ProVerif, и все остальные, уверен 💯, в таких аспектах:
- строгая семантика эквивалентности через гомотопии.
- моделирование сложных структур данных с зависимыми типами.
- интеграция с категориальной логикой для доказательства сложных свойств.
- гомотопическая эквивалентность позволяет строго моделировать инварианты протоколов.
- высшие индуктивные типы могут описывать сложные взаимодействия (например, распределённые протоколы).
=
Всё, с темкой разобрался, я красавчик :)
В заключение остаётся ещё подумать, какие сделать правильные выводы из этого всего.
Вообще, как я начал делать курсы по HoTT, в плане математики голова за считанные месяцы прямо ощутимо прокачалась чисто на базе этой теории.
Криптографические примитивы (шифрование, хэширование, подписи) моделируются через функции и уравнения. Символьная модель криптографии Долева-Яо, клаузы Хорна (привет, Пролог), по сути абстрактные методы анализа, которые авторы сами придумали:)
Сложные структуры данных (например, вложенные списки или рекурсивные типы) требуют ручного моделирования.
=> ProVerif будет более практичным -- для автоматического анализа криптографических протоколов в символической модели.
В HoTT же например, можно определить тип "протокол с условиями на последовательность шагов", которые автоматически проверяются системой, и так можно верифицировать протоколы с жёсткими структурными ограничениями,
HoTT интегрирует категориальную логику и теорию гомотопий -- мощные математические инструменты для доказательства свойств безопасности, что особенно полезно для анализа протоколов с распределённой логикой или сложными взаимодействиями (можно например формализовать, что протокол удовлетворяет условию инъективной эквивалентности.)
В общем, HoTT превосходит и ProVerif, и все остальные, уверен 💯, в таких аспектах:
- строгая семантика эквивалентности через гомотопии.
- моделирование сложных структур данных с зависимыми типами.
- интеграция с категориальной логикой для доказательства сложных свойств.
- гомотопическая эквивалентность позволяет строго моделировать инварианты протоколов.
- высшие индуктивные типы могут описывать сложные взаимодействия (например, распределённые протоколы).
=
Всё, с темкой разобрался, я красавчик :)
В заключение остаётся ещё подумать, какие сделать правильные выводы из этого всего.
Вообще, как я начал делать курсы по HoTT, в плане математики голова за считанные месяцы прямо ощутимо прокачалась чисто на базе этой теории.
👍31🤯12❤6🔥5
В заключение сериала про инструменты формальной верификации.
Да, вполне можно с ними поконкурировать, но для этого надо выстраивать серьёзный бизнес. Можно конечно делать верификацию и на Lean или Isabelle, кстати и на F*, но их формальные теории как я рассказал ↑ ↑ ↑ сильно проигрывают HoTT (вообще, Воеводский абсолютный гений computer science), а их экосистемы, по достаточно очевидным причинам, или совсем хиленькие или откровенно отстойные.
А вот связка Python (суперинженерная экосистема, с мощной поддержкой и символьных вычислений, и солверов, и функциональщины, и машинлёнинга...)
+ HoTT просто как маленькая библиотечка, получается просто огонь 💥
Посмотрите, какая будет возня если используете Coq + Galline :)
"Формальная верификация смарт-контрактов во фреймворке ConCert"
Но я с этим связываться точно не буду 💯
потому что, ну кто там заказчики догадаться несложно.
Например SELinux верифицированное ядро делалось по заказу Агентства нацбезопасности США. Верификация кода, криптоалгоритмов из этой же серии. Всяческий ЦэБэ или ГазМяс от них тоже недалеко ушёл.
Свяжешься с такими конторами -- не то что не заработаешь, а останешься сам им по уши должен и ещё будешь благодарить что не засадили в кутузку по итогу. Твой лепет "почему разработка софта - это сложно" серьёзные пацаны слушать вообще не будут 😎
C другой стороны связываться с чистой криптой мне просто физически противно 🤮
Как вариант крипто-игры
By 2026, the market for blockchain gaming is anticipated to have grown to $70 billion, an exponential growth rate.
но там ведь тоже каждый второй -- это гэмблинг кал 💩
Можно делать что-то типа расширенной версии тулзы статического анализа, но это уже совсем нишевое.
А главное должно быть -- чтобы это действительно было полезно итэ-массовке.
...
...Мышление письмом -- это лучший способ находить инсайты, особенно когда при этом можешь пообщаться с дипсинком жпт.
Придумал в процессе написания!!1 🚀 некоторые вещи конечно просто очевидны, именно поэтому их не замечаешь.
Заключительный пост сериала будет про это.
Да, вполне можно с ними поконкурировать, но для этого надо выстраивать серьёзный бизнес. Можно конечно делать верификацию и на Lean или Isabelle, кстати и на F*, но их формальные теории как я рассказал ↑ ↑ ↑ сильно проигрывают HoTT (вообще, Воеводский абсолютный гений computer science), а их экосистемы, по достаточно очевидным причинам, или совсем хиленькие или откровенно отстойные.
А вот связка Python (суперинженерная экосистема, с мощной поддержкой и символьных вычислений, и солверов, и функциональщины, и машинлёнинга...)
+ HoTT просто как маленькая библиотечка, получается просто огонь 💥
Посмотрите, какая будет возня если используете Coq + Galline :)
"Формальная верификация смарт-контрактов во фреймворке ConCert"
Но я с этим связываться точно не буду 💯
потому что, ну кто там заказчики догадаться несложно.
Например SELinux верифицированное ядро делалось по заказу Агентства нацбезопасности США. Верификация кода, криптоалгоритмов из этой же серии. Всяческий ЦэБэ или ГазМяс от них тоже недалеко ушёл.
Свяжешься с такими конторами -- не то что не заработаешь, а останешься сам им по уши должен и ещё будешь благодарить что не засадили в кутузку по итогу. Твой лепет "почему разработка софта - это сложно" серьёзные пацаны слушать вообще не будут 😎
C другой стороны связываться с чистой криптой мне просто физически противно 🤮
Как вариант крипто-игры
By 2026, the market for blockchain gaming is anticipated to have grown to $70 billion, an exponential growth rate.
но там ведь тоже каждый второй -- это гэмблинг кал 💩
Можно делать что-то типа расширенной версии тулзы статического анализа, но это уже совсем нишевое.
А главное должно быть -- чтобы это действительно было полезно итэ-массовке.
...
...Мышление письмом -- это лучший способ находить инсайты, особенно когда при этом можешь пообщаться с дипсинком жпт.
Придумал в процессе написания!!1 🚀 некоторые вещи конечно просто очевидны, именно поэтому их не замечаешь.
Заключительный пост сериала будет про это.
👍33🔥7❤4😁1
Идея -- Топологически-Ориентированное Проектирование (ТОП).
На основе HoTT сделать логический фреймворк, в рамках которого можно будет формально описывать и проектные требования, и конкретные архитектурные и софт-дизайнерские аспекты.
То есть предоставляется математически целостный формальный набор инструментов, который можно будет применять на самых разных уровнях: на этапе анализа, проектирования и реализации. Принципиально важно, что эти инструменты не просто какие-то эвристики программной инженерии, а математические абстракции, увязывающиеся друг с другом в систему с мощнейшим потенциалом.
И мы получим в итоге (достаточно) формальную спецификацию, на основе которой в идеальном случае можно будет автоматически сгенерировать код вместе с, например, триплами Хоара, а как минимум, будет прекрасное ТЗ для AI.
Мой курс вайб-проектирование уже неплохо работает, вчерашний отзыв:
Я прошёл курс по вайб-кодингу и сразу стал применять этот подход в одном из своих проектов в комбинации с BDD.
С помощью Qwen3 по шагам выполняю преобразования:
[ ... ]
Раньше я использовал ИИ как замену Google и StackOverflow. Теперь он превратился для меня в инструмент, которому не было аналогов. Вместо поиска информации ИИ выполняет часть работы: часть того, что он выдаёт сохраняется в проекте в той или иной форме.
По сути, должно получиться этакое усиленное BDD до уровня языков формальных спецификаций наподобие TLA+, или даже модел-чекинг (возможно, следующий сериал будет о нём :).
Ключевая фишка в том, что мы делаем не просто описания тест-кейсов на Gherkin как в голову взбрело самому умненькому/опытненькому (а вдруг такого нету?), а используем для этого строго ограниченный набор инструментов ТОП.
То есть, БАЗА: по сути, мы исходно имеем набор жёстких ограничений ТОП, который нам указывает что НЕ надо делать, и таким образом пространство возможных решений сокращается от бесконечности как сегодня в мейнстриме, до очень ограниченного количества возможностей, которое просчитает любой шахматист-второразрядник.
Причём здесь нету никаких конфликтов с эволюционным подходом, даже наоборот. Просто на каждом шаге на каждой итерации мы получаем крайне ограниченную возможность выбора последующих шагов (в идеале один). Ну как примерно когда вы пишите строку кода cтатической типизации, и чем ближе вы к концу инструкции, тем меньше количество возможностей вам предлагает автозаполнитель.
То есть ТОП это по сути просто такой набор гармонично связанных мета-понятий, которые мы используем при создании Gherkin-сценариев (да или любого другого DSL, по Алану Кэю), и который по определению никогда не даст вам свернуть не туда.
Мы не пишем сперва некоторый сценарий, а потом подыскиваем, что бы ему подошло из понятий ТОП, а сначала формулируем соответствующее множество понятий под задачу, и уже затем в рамках строгих соответствующих ограничений пишем словесные описания.
Ну вот, навскидку, скриншоты возможных сценариев (писал AI, и на таком уровне Клод 4 например будет очень хорошим ассистентом)
(знаете кстати, как можно быстро понять что текст писал AI? он любит начинать фразы с "Это...")
На основе HoTT сделать логический фреймворк, в рамках которого можно будет формально описывать и проектные требования, и конкретные архитектурные и софт-дизайнерские аспекты.
То есть предоставляется математически целостный формальный набор инструментов, который можно будет применять на самых разных уровнях: на этапе анализа, проектирования и реализации. Принципиально важно, что эти инструменты не просто какие-то эвристики программной инженерии, а математические абстракции, увязывающиеся друг с другом в систему с мощнейшим потенциалом.
И мы получим в итоге (достаточно) формальную спецификацию, на основе которой в идеальном случае можно будет автоматически сгенерировать код вместе с, например, триплами Хоара, а как минимум, будет прекрасное ТЗ для AI.
Мой курс вайб-проектирование уже неплохо работает, вчерашний отзыв:
Я прошёл курс по вайб-кодингу и сразу стал применять этот подход в одном из своих проектов в комбинации с BDD.
С помощью Qwen3 по шагам выполняю преобразования:
[ ... ]
Раньше я использовал ИИ как замену Google и StackOverflow. Теперь он превратился для меня в инструмент, которому не было аналогов. Вместо поиска информации ИИ выполняет часть работы: часть того, что он выдаёт сохраняется в проекте в той или иной форме.
По сути, должно получиться этакое усиленное BDD до уровня языков формальных спецификаций наподобие TLA+, или даже модел-чекинг (возможно, следующий сериал будет о нём :).
Ключевая фишка в том, что мы делаем не просто описания тест-кейсов на Gherkin как в голову взбрело самому умненькому/опытненькому (а вдруг такого нету?), а используем для этого строго ограниченный набор инструментов ТОП.
То есть, БАЗА: по сути, мы исходно имеем набор жёстких ограничений ТОП, который нам указывает что НЕ надо делать, и таким образом пространство возможных решений сокращается от бесконечности как сегодня в мейнстриме, до очень ограниченного количества возможностей, которое просчитает любой шахматист-второразрядник.
Причём здесь нету никаких конфликтов с эволюционным подходом, даже наоборот. Просто на каждом шаге на каждой итерации мы получаем крайне ограниченную возможность выбора последующих шагов (в идеале один). Ну как примерно когда вы пишите строку кода cтатической типизации, и чем ближе вы к концу инструкции, тем меньше количество возможностей вам предлагает автозаполнитель.
То есть ТОП это по сути просто такой набор гармонично связанных мета-понятий, которые мы используем при создании Gherkin-сценариев (да или любого другого DSL, по Алану Кэю), и который по определению никогда не даст вам свернуть не туда.
Мы не пишем сперва некоторый сценарий, а потом подыскиваем, что бы ему подошло из понятий ТОП, а сначала формулируем соответствующее множество понятий под задачу, и уже затем в рамках строгих соответствующих ограничений пишем словесные описания.
Ну вот, навскидку, скриншоты возможных сценариев (писал AI, и на таком уровне Клод 4 например будет очень хорошим ассистентом)
(знаете кстати, как можно быстро понять что текст писал AI? он любит начинать фразы с "Это...")
✍29😁13🏆5💯4🤔1
Сейчас в разгаре первая волна итэ-демобилизации: стремительно исчезает вся эта беловоротничковая шушера (бухгалтеры юристы психологи администраторы дикторы телеведущие колл-центры...). Им на смену пришёл жпт.
При этом стремительно набирает ход вторая волна итэ-демобилизации: заменяются или достаточно скоро начнут заменяться синие воротнички (строители курьеры таксисты слесари плотники кладовщики грузчики дальнобойщики электрики сварщики водолазы крановщики...). Им на смену по всему миру активно приходят роботы.
Мой прогноз: до конца текущего десятилетия роботы станут естественны, как сегодня жпт в первой волне.
Следом будет заключительная, всеобщая итэ-демобилизация: на условных "Алис" и всяческих киборгов будут окончательно заменены учителя врачи чиновники лётчики полицейские военные и спецслужбы.
Мой прогноз: до 2035-го станут естественны войны роботов (как между государствами так и между криптохакерскими структурами). Причём они будут происходить на скоростях, буквально неподвластных человеческому зрению и мышлению. Например, мириады дронов схлестнулись на доли секунды -- и уже понятно кто выиграл. Далее, соответственно, быстрый раш, только базу противника не ломаем, а захватываем.
И наконец самыми последними будут заменены программисты: потому что едва это произойдёт, что означает что AI научится кодить, как сеньор, он тут же начнёт рекурсивное самоулучшение, и просто по определению случится технологическая сингулярность.
Сроки? Максимум 2042-й год.
Думайте.
При этом стремительно набирает ход вторая волна итэ-демобилизации: заменяются или достаточно скоро начнут заменяться синие воротнички (строители курьеры таксисты слесари плотники кладовщики грузчики дальнобойщики электрики сварщики водолазы крановщики...). Им на смену по всему миру активно приходят роботы.
Мой прогноз: до конца текущего десятилетия роботы станут естественны, как сегодня жпт в первой волне.
Следом будет заключительная, всеобщая итэ-демобилизация: на условных "Алис" и всяческих киборгов будут окончательно заменены учителя врачи чиновники лётчики полицейские военные и спецслужбы.
Мой прогноз: до 2035-го станут естественны войны роботов (как между государствами так и между криптохакерскими структурами). Причём они будут происходить на скоростях, буквально неподвластных человеческому зрению и мышлению. Например, мириады дронов схлестнулись на доли секунды -- и уже понятно кто выиграл. Далее, соответственно, быстрый раш, только базу противника не ломаем, а захватываем.
И наконец самыми последними будут заменены программисты: потому что едва это произойдёт, что означает что AI научится кодить, как сеньор, он тут же начнёт рекурсивное самоулучшение, и просто по определению случится технологическая сингулярность.
Сроки? Максимум 2042-й год.
Думайте.
3🤯34😁25🤔9🐳7🔥6
This media is not supported in your browser
VIEW IN TELEGRAM
Не люблю и не планирую никогда учить в итэ ничему, отличающемуся от сеньорского архитекторского -- имею в виду тимлидство, техдирство и т.д., буквально зарекаюсь. И давно уже бросил консультировать, но иногда прям грустно, беспредел может быть ведь и с другой стороны.
Дорогие, ну всё же смотрите по ситуации, если босс искренне старается, горит душой, зачем таких разводить-то, это тоже западло.
Старый знакомый, сам вообще не айтишник, из военных, с инвалидностью, задумал киллер контрал-страйка (вот почему меня хотя бы не спросил? я бы прям очень жёстко сразу отговорил). Его для начала раскрутили на покупку какого-то дорогого движка за пять зелёных штук, влез в долги... Бюджет инвесторов сливается, продукт на полгода отстаёт и даже альфа-версии не видно, и уже скоро придут серьёзные пацаны с вопросом "где деньги?"...
Дорогие боссы, БАЗА: подчинённые вас в 100% наёбывают (и в принципе в 98% правильно делают, и я учу и буду продолжать, как это делать правильно, но это другое). Вешают вам лапшу насколько это трудно, сроки говорят с запасом в 2-5-11 раз, а вы мямлите "ммну ладно"...
Вот что должно быть в вашей команде в первую очередь, если у вас не было опыта сеньорства:
Программисты должны еженедельно мучительно доказывать КАЖДЫЙ стори-поинт на общем собрании.
Не знаете что это, спросите жпт.
Сделайте премии побольше, а зп поменьше, и увязывайте премию напрямую с поинами.
Причём это не то что "а давайте Олегу дадим три пойнта, а Оксане пять", нет.
Даже одно очко должно быть ОЧЕНЬ трудно получить :)
Наймите со стороны любого сеньора с хорошими разговорными брутал-скиллами, пусть он раз в неделю активно поприсутствует на ваших созвонах.
Не бойтесь, сегодня никуда разработчики не разбегутся, покряхтят и начнут работать как надо.
А вам, программисты, надо быть Человеками прежде всего (с капиталистами-то всё ясно, они по дефолту идут в ад). А не то...
Дорогие, ну всё же смотрите по ситуации, если босс искренне старается, горит душой, зачем таких разводить-то, это тоже западло.
Старый знакомый, сам вообще не айтишник, из военных, с инвалидностью, задумал киллер контрал-страйка (вот почему меня хотя бы не спросил? я бы прям очень жёстко сразу отговорил). Его для начала раскрутили на покупку какого-то дорогого движка за пять зелёных штук, влез в долги... Бюджет инвесторов сливается, продукт на полгода отстаёт и даже альфа-версии не видно, и уже скоро придут серьёзные пацаны с вопросом "где деньги?"...
Дорогие боссы, БАЗА: подчинённые вас в 100% наёбывают (и в принципе в 98% правильно делают, и я учу и буду продолжать, как это делать правильно, но это другое). Вешают вам лапшу насколько это трудно, сроки говорят с запасом в 2-5-11 раз, а вы мямлите "ммну ладно"...
Вот что должно быть в вашей команде в первую очередь, если у вас не было опыта сеньорства:
Программисты должны еженедельно мучительно доказывать КАЖДЫЙ стори-поинт на общем собрании.
Не знаете что это, спросите жпт.
Сделайте премии побольше, а зп поменьше, и увязывайте премию напрямую с поинами.
Причём это не то что "а давайте Олегу дадим три пойнта, а Оксане пять", нет.
Даже одно очко должно быть ОЧЕНЬ трудно получить :)
Наймите со стороны любого сеньора с хорошими разговорными брутал-скиллами, пусть он раз в неделю активно поприсутствует на ваших созвонах.
Не бойтесь, сегодня никуда разработчики не разбегутся, покряхтят и начнут работать как надо.
А вам, программисты, надо быть Человеками прежде всего (с капиталистами-то всё ясно, они по дефолту идут в ад). А не то...
👍40🫡14💯5✍4🐳2
С одной стороны, эту тему я немного продумал, получается топчик. Даже совсем детский пример "сделать игру три-в-ряд" на моём hott-движке, вот как можно подходить к проектированию, навскидку:
-- в архитектурном плане это State Machine (n-мерный тор) на основе гомотопий с поддержкой обмена сообщениями (гомотопии на поверхности тора описывают переходы между состояниями);
-- доска (GridState, состояние сетки 8x8) -- точка в пространстве, переходы между которыми моделируются гомотопическими путями (ходами игрока);
-- спецэффекты(например, удаление всех элементов одного типа) моделируем высшими индуктивными типами (базовые точки как активация бонуса, и пути, влияющие на GridState);
-- комбинации из 3+ одинаковых элементов в рядах/столбцах -- гомотопический инвариант (группа), автоматическая трассировка для обнаружения эквивалентных конфигураций;
-- подсчёт очков -- дискретная точка без внутренней структуры (TruncationLevel.0). Принцип унивалентности позволяет легко и просто менять эквивалентные сценарии (например, разные комбинации с одинаковой стоимостью);
-- завершение игры -- когда все возможные ходы стягиваются в одну точку, исключающую дальнейшие переходы (UniverseLevel.-1).
...только тут есть малюсенький крохотный нюанс, что для этого мыслить надо, хорошо погрузившись в хотт, для чего пройти соответствующие курсы конечно будет недостаточно — но чтобы просто их пройти надо добраться где-то примерно до аспирантского уровня...
мы со святым Робертом Милнером (автор LCF, ML-языки, пи-исчисление...) визуально стали почти неотличимы, и это радует :)
смиренно преклоняюсь к трудам гуру как к его стопам 🙏
-- в архитектурном плане это State Machine (n-мерный тор) на основе гомотопий с поддержкой обмена сообщениями (гомотопии на поверхности тора описывают переходы между состояниями);
-- доска (GridState, состояние сетки 8x8) -- точка в пространстве, переходы между которыми моделируются гомотопическими путями (ходами игрока);
-- спецэффекты(например, удаление всех элементов одного типа) моделируем высшими индуктивными типами (базовые точки как активация бонуса, и пути, влияющие на GridState);
-- комбинации из 3+ одинаковых элементов в рядах/столбцах -- гомотопический инвариант (группа), автоматическая трассировка для обнаружения эквивалентных конфигураций;
-- подсчёт очков -- дискретная точка без внутренней структуры (TruncationLevel.0). Принцип унивалентности позволяет легко и просто менять эквивалентные сценарии (например, разные комбинации с одинаковой стоимостью);
-- завершение игры -- когда все возможные ходы стягиваются в одну точку, исключающую дальнейшие переходы (UniverseLevel.-1).
...только тут есть малюсенький крохотный нюанс, что для этого мыслить надо, хорошо погрузившись в хотт, для чего пройти соответствующие курсы конечно будет недостаточно — но чтобы просто их пройти надо добраться где-то примерно до аспирантского уровня...
смиренно преклоняюсь к трудам гуру как к его стопам 🙏
🤓34👍13🤯6👏5🤔3
...Более того, у многих не получается создать что-то работающее даже просто в модели обмена сообщениями (база: изучайте 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 шага ключевые. Хочу продемонстрировать вживую и, главное, "научать", как можно с самого начала и на всю перспективу удерживать линейной сложность программного кода с логикой взаимодействия тысяч типов сущностей в реальном времени даже для неоднозначного и нечёткого ТЗ с постоянными новыми хотелками.
И главное, чтобы это было доступно любому миддлу, этих ваших универов не заканчивавшего.
...и более того, на моём ключевом практическом курсе трека объектно-ориентированного проектирования ребята-миддлы в итоге подчас запутываются даже в небольшом проекте на пару десятков абстрактных типов данных...
Признаю, это полностью моя недоработка 💯
как закончу второй курс по гомотопической теории, плотно прям берусь за доработку практики ООАП, забустим её моделью акторов Хьюитта.
HoTT же, думаю, останется навсегда лишь для самых умненьких (только 0,002% способны.... :).
=
Software/System Design -- это про то что вне зависимости от объёма вашего проекта у вас обязательно там и тут будут образовываться big balls of mud конкретно в вашем коде. И тут важно эксплицитно разделять три типа этого дерьма:
-- DevOps и System Design in Large: бесконечные архитектурные боли и страдания , связанные с интеграцией чужих каках (все эти опенсорсные либы, микросервисы брокеры балансировщики очереди куберы-шмуберы), подчас вообще чистый devops, который сегодня стало модным скидывать на чистых разработчиков;
-- System Design in Small: технические
-- 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 шага ключевые. Хочу продемонстрировать вживую и, главное, "научать", как можно с самого начала и на всю перспективу удерживать линейной сложность программного кода с логикой взаимодействия тысяч типов сущностей в реальном времени даже для неоднозначного и нечёткого ТЗ с постоянными новыми хотелками.
И главное, чтобы это было доступно любому миддлу, этих ваших универов не заканчивавшего.
👍42❤🔥8❤5🔥2😁2
Дон Хуан из микрософта классный пост:
"Грядущая революция искусственного интеллекта в распределённых системах"
Как AI создал точные формальные спецификации TLA + из исходного кода Azure Storage, и затем выявил тонкий баг, который не сдавался классическим code review и тотальному тестированию.
Да, пока AI не так хорош в проектировании концептуальной системной архитектуры. Но дело в том, что большинство программистов также не так хороши в этом, а 98% уже значительно хуже AI.
AI постоянно галлюцинирует? Да вообще не имеет значения, что AI "не знает", что он делает, не понимает смысла создаваемого. В большинстве случаев мы сами тоже этого не знаем.
И с твоим проектом в итоге либо всё будет хорошо, либо нет. Одно из двух.
"Грядущая революция искусственного интеллекта в распределённых системах"
Как AI создал точные формальные спецификации TLA + из исходного кода Azure Storage, и затем выявил тонкий баг, который не сдавался классическим code review и тотальному тестированию.
Да, пока AI не так хорош в проектировании концептуальной системной архитектуры. Но дело в том, что большинство программистов также не так хороши в этом, а 98% уже значительно хуже AI.
AI постоянно галлюцинирует? Да вообще не имеет значения, что AI "не знает", что он делает, не понимает смысла создаваемого. В большинстве случаев мы сами тоже этого не знаем.
И с твоим проектом в итоге либо всё будет хорошо, либо нет. Одно из двух.
👍52😁8❤2
.
"Всё что нужно знать про Entity-Component-System"
(геймдев открывает для себя функциональное программирование:)
Ну, да, для системы с тысячами типов данных, как dwarf fortress, ECS + реляционная модель, "усиленная" джсонами.
Связи через графовые отношения:
Да вот только тривиальное "найти всех гномов в радиусе 10м, держащих деревянный меч", систему сразу подвесит :) Я бы ещё для хардкора DDD накинул, чтобы только первичные требования составлять пару лет (и через месяц реализации понять, что надо было делать совсем по другому ).
-- Реактивщина + стрим процессинг?
Чисто лучше, да только помрёшь в отладке асинхронных цепочек событий )))
Поэтому и от модели акторов я наверное всё же откажусь.
"Возьми кафку", говорили они...
-- Онтика? RDF/OWL?
+ SPARQL-ом "найти материалы, которые ржавеют при контакте с водой"
Пихаем всё графом в Neo4j...
да только оверхэд на инференс в реалтайме получаем уже на первых 50 сущностях :)
Разве что на Rust + Bevy пилить, да тут сам загнёшься соответственно от когнитивный перегрузки.
Родной df на плюсах, на райзене 5600 и так-то большой тормоз уже на паре сотен дварфов и сотне прирученных животных (и уж молчу про симуляцию магмы :)
-- На виртуально бесконечных ресурсах я бы выбрал скорее всего Event Sourcing + CQRS, тут не просто отладка элементарная, а мы вообще получаем по сути детерминированную машину времени, и решаем кучу проблем.
Собственно вот:
Domain-Driven Design: The Power of CQRS and Event Sourcing
Да только на практике в таком подходе заткнёмся ещё быстрее, чем с онтологиями...
-- На самом деле наиболее легко и просто было бы такое спроектировать просто в чистом ФП, да только из-за иммутабельности тоже совсем не потянет в плане продуктивности.
Размышления продолжаю.
"Всё что нужно знать про 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
Да только на практике в таком подходе заткнёмся ещё быстрее, чем с онтологиями...
-- На самом деле наиболее легко и просто было бы такое спроектировать просто в чистом ФП, да только из-за иммутабельности тоже совсем не потянет в плане продуктивности.
Размышления продолжаю.
👍39🤔17❤2
Линзы кстати неплохая темка: когда мы фокусируемся на части структуры данных (своеобразная инкапсуляция геттеров и сеттеров в одной сущности).
Линзы неплохо обобщаются через профункторы: один интерфейс для разных операций; сложные операции выражаются через простую композицию "оптических элементов" (условно, как в гомоморфном шифровании).
А профункторная оптика, соответственно, расширяется до рефлексивной, и мы попадаем в мета-программирование.
Оптику можно строить во время выполнения, генерация кода, конфигурируемые проекции.
Игрок может задавать собственные запросы... Но тоже нагрузочно конечно.
На хаскеле это всё красиво выглядит, но страшно далёк он от трудового итэ-народа.
Линзы неплохо обобщаются через профункторы: один интерфейс для разных операций; сложные операции выражаются через простую композицию "оптических элементов" (условно, как в гомоморфном шифровании).
А профункторная оптика, соответственно, расширяется до рефлексивной, и мы попадаем в мета-программирование.
-- Рефлексивное описание дварфа
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)
Оптику можно строить во время выполнения, генерация кода, конфигурируемые проекции.
Игрок может задавать собственные запросы... Но тоже нагрузочно конечно.
На хаскеле это всё красиво выглядит, но страшно далёк он от трудового итэ-народа.
🤔40🤯9❤6
Почему SaaS сегодня -- это проигрышная бизнес-модель?
Чтобы заключать крупные сделки, нужны корпоративные продажи (организовать такой процесс крайне тяжело), продвинутая техподдержка, постоянная кастомизация -- все те скучные и не требующие обслуживания вещи, с которыми так хорошо справляются Яндекс и Мэйл. Ещё в девяностые был случай, знакомой накодил опердень и ходил соло ставил по банкам триал на 60 дней. В одном банке триал закончился, а у них уже работа на нём ведётся, ему звонят "срочно!", он говорит "ну так надо же оплатить", после чего к нему приехали хмурые пацаны в кожаных куртках и сказали: финансовыми вопросами разбирайтесь сами, но банк должен сегодня заработать :)
Сегодня это впрочем стало цивилизованно: юристы просто придушат, и будешь по жизни поддерживать свой SaaS для таких забесплатно.
=
Если же будете ориентироваться на клиентов поменьше, то быстро поймёте, что SaaS -- это буквально гонка на выживание. Сегодная AI + low/no code развивается так быстро, что условный ООО/ИП 100500 раз подумает, стоит ли вкладывать в ваш продукт 10,000 рублей, вместо того чтобы за 2,000 рублей взять подписку на Клода 4, который сразу закодит 80% требований, или купить более дешёвый клон вашего продукта, который какой-то студентик запилил за 48 часов.
=
Cегодня у заказчиков-айтишников SaaS просто ещё считается "более настоящим" итэ-бизнесом, нежели условный "консалтинговый бизнес", но этот снобизм с развитием AI через годик полностью исчезнет.
Чтобы заключать крупные сделки, нужны корпоративные продажи (организовать такой процесс крайне тяжело), продвинутая техподдержка, постоянная кастомизация -- все те скучные и не требующие обслуживания вещи, с которыми так хорошо справляются Яндекс и Мэйл. Ещё в девяностые был случай, знакомой накодил опердень и ходил соло ставил по банкам триал на 60 дней. В одном банке триал закончился, а у них уже работа на нём ведётся, ему звонят "срочно!", он говорит "ну так надо же оплатить", после чего к нему приехали хмурые пацаны в кожаных куртках и сказали: финансовыми вопросами разбирайтесь сами, но банк должен сегодня заработать :)
Сегодня это впрочем стало цивилизованно: юристы просто придушат, и будешь по жизни поддерживать свой SaaS для таких забесплатно.
=
Если же будете ориентироваться на клиентов поменьше, то быстро поймёте, что SaaS -- это буквально гонка на выживание. Сегодная AI + low/no code развивается так быстро, что условный ООО/ИП 100500 раз подумает, стоит ли вкладывать в ваш продукт 10,000 рублей, вместо того чтобы за 2,000 рублей взять подписку на Клода 4, который сразу закодит 80% требований, или купить более дешёвый клон вашего продукта, который какой-то студентик запилил за 48 часов.
=
Cегодня у заказчиков-айтишников SaaS просто ещё считается "более настоящим" итэ-бизнесом, нежели условный "консалтинговый бизнес", но этот снобизм с развитием AI через годик полностью исчезнет.
👍32🤔13😁5🔥3
Облако драгоценностей за неделю.
Основной паблик:
...Всего этого можно было избежать, если бы разработчики исходили из того, что любые их радужные предположения, скорее всего, неверны, а самым главным ошибочным из них будет представление о том, что всё будет идеально, ну или хотя бы "как и вчера".
Для донов-начинающих:
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, архитектура на монадах состояний и т.д.
Добавлю ещё штук пять стилей, включая упоминавшиеся, этим летом 💯
Основной паблик:
...Всего этого можно было избежать, если бы разработчики исходили из того, что любые их радужные предположения, скорее всего, неверны, а самым главным ошибочным из них будет представление о том, что всё будет идеально, ну или хотя бы "как и вчера".
Для донов-начинающих:
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, архитектура на монадах состояний и т.д.
Добавлю ещё штук пять стилей, включая упоминавшиеся, этим летом 💯
❤46👍6
Сегодня прекрасный, Духов день 🙏 (всегда бывает дождик, кстати)!
Батюшки по всей Москве изгоняют AI-бесов из уличных роботов 👊
Мне приснилось, как я лечу в небе высоко в облаках, как Гум-Гам 😇
Кстати очень рекомендую, прочитайте своим детишкам эту светлую фантастическую повесть из 1970-го, советского святого писателя Евгения Велтистова (сперва книга, потом фильм): пророческое, как AI АВТУК порабощал людей.
Батюшки по всей Москве изгоняют AI-бесов из уличных роботов 👊
Мне приснилось, как я лечу в небе высоко в облаках, как Гум-Гам 😇
Кстати очень рекомендую, прочитайте своим детишкам эту светлую фантастическую повесть из 1970-го, советского святого писателя Евгения Велтистова (сперва книга, потом фильм): пророческое, как AI АВТУК порабощал людей.
👍41😁15✍5🔥2🤯1
(сегодня буду много постов размышлять текстом, важная тема, потерпите пожалуйста 🙏🙏🙏)
Сейчас тренд на всё своё "доморощенное"(в целом совершенно правильный, без иронии, я ещё с 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. Вся академическая Европа и США сидит в основном на нём, и нам по определению на это теперь путь заказан.
Риторическое: надо ли делать "свой солвер", "свой пруф-ассистант", "свой формальный верификация"? При том, что последние топовые математики в этих темах уехали в европы...
Я кстати послезавтра Школу закрываю, серьёзно. Уже началисьгонения штрафы онлайн-школ, кто без образовательной лицензии работает; принципиально не буду получать. В Индии например государство только поддерживает энтузиастов айти-обучения...
Сейчас тренд на всё своё "доморощенное"
"свой ОС" "свой геймдев движок" "свой смартфон" "свой мессенджер" "свой проц" "свой приставка" "свой AI"...
Даже появилась "свой IDE"
Хотя странно рассуждать о полноценном развитии "своего итэ", если оно не происходит прежде всего на базе своих фундаментальных разработок. Например, интел однажды слил полмиллиарда долларов из-за неверного проектирования чипа, и теперь активно применяет для этого всяческие системы верификации, включая SAT/SMT-солверы (формальные решатели). Как думаете, наши СБИС на каком софте проектируются, и насколько теперь ему можно доверять? А сегодня доля верификации в бюджетах таких проектов -- до 70% затрат на разработку СБИС.
Кстати, и рынок верификации смарт-контрактов с нынешних $300 млн. к 2030-му вырастет примерно в 7 раз, а у нас цифровой рубль, планируется крипту разрешить...
Но конечно никакого даже "свой солвер" нету и помине; в Стеклова и универах пользуют только зарубежные, вроде микрософтовского Z3
Например, лекция микро-курс по SAT/SMT делал в МГУ приглашённый индус Vijay Ganesh. Хотя, по большому счёту, это уровень дипломного проекта, ну максимум аспирантского.
И уж тем более по формализации математики пустота. Филдсовский лауреат Tao вон буквально упарывается в обучении математиков современным it, и ключевой акцент, конечно, на proof assistant-ах и языках с завтипами: Coq, Lean, Agda, Isabelle, F*, Idris...
Coq ведь начинался усилиями советского математика Владимира Воеводского (гомотопическая теория типов), и посмотрите, что он сегодня представляет после ребрендинга: Rocq Prover. Вся академическая Европа и США сидит в основном на нём, и нам по определению на это теперь путь заказан.
Риторическое: надо ли делать "свой солвер", "свой пруф-ассистант", "свой формальный верификация"? При том, что последние топовые математики в этих темах уехали в европы...
Я кстати послезавтра Школу закрываю, серьёзно. Уже начались
✍38❤16🔥6😁3👌3
...Так-то мне это просто сильно интересно, поэтому в любом случае продолжу впроголодь развивать парадигму топологически-ориентированного программирования на базе гомотопической теории типов. Мой подход пока хотя и учебный, но чисто технически/архитектурно потенциал его несравненно выше существующих пруф-ассистантов и теорем-пруверов, потому что они сами по себе фактически полузакрытые фреймворки, где требуется огромное количество ручного ввода, а интеграция с чем-то внешним серьёзно затруднена. Верификация кода на 5,000 строк требует 200,000 строк кода доказательств :)
А хорошо бы более активно и солверы, особенно свои, применять для автоматического поиска доказательства и стыковки с AI:
- обучение на существующих формализованных доказательствах;
- генерация подсказок и дополнений при построении доказательств;
- приближение языка формализации к обычному математическому;
- более понятная визуализация доказательств
и т д и т п.
Стратегически в планах сделать (причём именно в таком порядке)
1 "свой формальный верификация"
2 "свой пруф-ассистант"
3 "свой солвер"
Солвер же это на сегодня задача по сути чисто техническая, никаких питонов, сразу надо делать скоростную версию на rust. Но там такая логика, что для реальных проектов нужна оперативка на сотни гигов, для возни с булевыми формулами. Никогда уже не накоплю на раб.станцию, на последние гроши взял свежую книжечку "Введение в алгебраическую топологию" (лекции на мехмате МГУ, в Новосибе: симплициальные, сингулярные и клеточные гомологии, связь с гомотопическими группами клеточных пространств, кольцо когомологий, двойственность Пуанкаре...). Не исключено, что сильная математическая база вполне может снять кучу технических проблем.
А хорошо бы более активно и солверы, особенно свои, применять для автоматического поиска доказательства и стыковки с AI:
- обучение на существующих формализованных доказательствах;
- генерация подсказок и дополнений при построении доказательств;
- приближение языка формализации к обычному математическому;
- более понятная визуализация доказательств
и т д и т п.
Стратегически в планах сделать (причём именно в таком порядке)
1 "свой формальный верификация"
2 "свой пруф-ассистант"
3 "свой солвер"
Солвер же это на сегодня задача по сути чисто техническая, никаких питонов, сразу надо делать скоростную версию на rust. Но там такая логика, что для реальных проектов нужна оперативка на сотни гигов, для возни с булевыми формулами. Никогда уже не накоплю на раб.станцию, на последние гроши взял свежую книжечку "Введение в алгебраическую топологию" (лекции на мехмате МГУ, в Новосибе: симплициальные, сингулярные и клеточные гомологии, связь с гомотопическими группами клеточных пространств, кольцо когомологий, двойственность Пуанкаре...). Не исключено, что сильная математическая база вполне может снять кучу технических проблем.
2✍44🔥9🏆4😁3
Почему я у всех этих западных пруверов-шмуверов (далее - Эти) потенциально выигрываю архитектурно? И насколько вообще мои оценки адекватны?
Ну, сегодня к счастью есть достаточно объективные AI-консультанты, шарящие в математике весьма уверенно (вдобавок, напомню, математика существенно проще чем программирование). Я спрашивал и у клода+опуса 4, и у гемини 2.5, и у дипсика и квена с дипсинками, показывал им свой код, и получил очень позитивный фидбэк. Основные претензии чисто у вас недоделано вот тут, а технически не хватает вот этого и того, ну дык, это уже дело времени. Реально очень доволен, даже сам не ожидал 🙏
Потому что всё Это ихнее делалось с нуля, вообще без опыта подобных проектов, а внутри, может их гитхабы посмотреть, это тотальное говнолегаси, которое писали не программисты-архитекторы с многолетним опытом, а преимущественно математики, да ещё и подчас на хаскелях! 🫢
Coq (индуктивные типы и тактики), Isabelle/HOL, Lean основаны на "классических" теориях типов или логике высшего порядка, и вполне обходятся без унивалентности (самая мякотка гомотопической теории). Унивалентность позволяет рассматривать равенство как эквивалентность (изоморфизм) между объектами, что крайне полезно при проверке соответствия интерфейсов или в модел-чекинге.
Я только-только вчера добавил транспорты между путями в ТОП: автоматическое перемещение между "равными" объектами без необходимости явного (ручного) доказательства инвариантов. А у Этих требуется доказывать корректность программ относительно их спецификаций через явные отношения между объектами (изоморфизмы, биекции...), писать крайне громоздкие конструкции для выражения эквивалентности (аксиомы выбора, дополнительные предикаты...). А я потенциально могу работать вообще со "структурами до изоморфизма" (например, в теоркате, при верификации распределённых систем, c гомотопическими типами...).
Кроме того, дальше вообще без проблем добавить "кубики" (чтобы строить модели в конструктивной метатеории, через конструктивную интерпретацию равенства эквивалентных типов), а этот ваш Lean 4 вообще на такое не способен, ну или через кривые приляпки, потому что его реализация использует UIP (Uniqueness of Identity Proofs), что противоречит принципам HoTT, где равенства -- это пути в гомотопическом пространстве (+ кубическая теория позволяет манипулировать "равенствами" напрямую, через операции и композицию 💪🏻 ).
Ну, сегодня к счастью есть достаточно объективные AI-консультанты, шарящие в математике весьма уверенно (вдобавок, напомню, математика существенно проще чем программирование). Я спрашивал и у клода+опуса 4, и у гемини 2.5, и у дипсика и квена с дипсинками, показывал им свой код, и получил очень позитивный фидбэк. Основные претензии чисто у вас недоделано вот тут, а технически не хватает вот этого и того, ну дык, это уже дело времени. Реально очень доволен, даже сам не ожидал 🙏
Потому что всё Это ихнее делалось с нуля, вообще без опыта подобных проектов, а внутри, может их гитхабы посмотреть, это тотальное говнолегаси, которое писали не программисты-архитекторы с многолетним опытом, а преимущественно математики, да ещё и подчас на хаскелях! 🫢
Coq (индуктивные типы и тактики), Isabelle/HOL, Lean основаны на "классических" теориях типов или логике высшего порядка, и вполне обходятся без унивалентности (самая мякотка гомотопической теории). Унивалентность позволяет рассматривать равенство как эквивалентность (изоморфизм) между объектами, что крайне полезно при проверке соответствия интерфейсов или в модел-чекинге.
Я только-только вчера добавил транспорты между путями в ТОП: автоматическое перемещение между "равными" объектами без необходимости явного (ручного) доказательства инвариантов. А у Этих требуется доказывать корректность программ относительно их спецификаций через явные отношения между объектами (изоморфизмы, биекции...), писать крайне громоздкие конструкции для выражения эквивалентности (аксиомы выбора, дополнительные предикаты...). А я потенциально могу работать вообще со "структурами до изоморфизма" (например, в теоркате, при верификации распределённых систем, c гомотопическими типами...).
Кроме того, дальше вообще без проблем добавить "кубики" (чтобы строить модели в конструктивной метатеории, через конструктивную интерпретацию равенства эквивалентных типов), а этот ваш Lean 4 вообще на такое не способен, ну или через кривые приляпки, потому что его реализация использует UIP (Uniqueness of Identity Proofs), что противоречит принципам HoTT, где равенства -- это пути в гомотопическом пространстве (+ кубическая теория позволяет манипулировать "равенствами" напрямую, через операции и композицию 💪🏻 ).
1🏆30🔥16🤔5😁2
-- Сергей Игоревич, но ведь можно и без 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 - как математически обобщённая ТО.
Конечно, и это успешно делается десятилетиями (за многие миллионы долларов :)
Так или иначе, классические основания покрывают >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 - как математически обобщённая ТО.
✍33🏆12❤5😁3
(заключительное и спасибо за внимание; всё додумал с вашей помощью ❤️❤️❤️)
Насколько это всё серьёзно?
Навскидку, это прежде всего военные и аэрокосмические контракты, типа "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 шагов).
В тему: "Ехали тьюрмиты и тримувьи на машите Тьюринга"
Насколько это всё серьёзно?
Навскидку, это прежде всего военные и аэрокосмические контракты, типа "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 шагов).
В тему: "Ехали тьюрмиты и тримувьи на машите Тьюринга"
2🤯40✍8🏆4😁2❤1