Немного поигрался с лямбда-кубом Барендрегта, пошёл сверху вниз:
CoC я реализовал в 70 строк F#,
затем запилил System Fω (F-омега)
(полиморфизм + конструкторы типов высшего порядка),
затем λP2 (зависимые типы + полиморфизм),
а вот на λPω (зависимые типы + конструкторы типов) сломался.
Просто так полиморфизм из CoC не удалить (Кокан всё же не дурак), надо выстраивать строгую иерархию типов, индексы де Брёйна и всё подобное; по сути надо полностью заменить универсальную архитектуру на иерархическую + жёсткую типизацию.
С другой стороны и хорошо что не вышло, всё равно этот куб на практике не актуален, а CoC и HoTT я реализовал, и куда важнее кубическую теорию дальше (успеть) сделать -- чётко под задачи программиста-миддла. Хотя бы научить рассуждать in small в соответствующих моделях. Например, цепочка конвертации данных с помощью унивалентности (композиция путей соответствует композиции эквивалентностей) с автоматическим доказательством коммутативности преобразований. И постепенно выходим на уровень формального мышления in large.
А без понимания теории типов все проекты будут получаться как на картинке,
но я уже совсем один остался в России в этих темках куда-то ещё едва бреду.....
все уснули давно
в километрах глубин
никого ничего он остался один....
кто сказал что нельзя
переплыть океан
это грустная шутка это хитрый обман...
я сумею доплыть
под сияние звёзд
я хочу увидать край где много берёз...
CoC я реализовал в 70 строк F#,
затем запилил System Fω (F-омега)
(полиморфизм + конструкторы типов высшего порядка),
затем λP2 (зависимые типы + полиморфизм),
а вот на λPω (зависимые типы + конструкторы типов) сломался.
Просто так полиморфизм из CoC не удалить (Кокан всё же не дурак), надо выстраивать строгую иерархию типов, индексы де Брёйна и всё подобное; по сути надо полностью заменить универсальную архитектуру на иерархическую + жёсткую типизацию.
С другой стороны и хорошо что не вышло, всё равно этот куб на практике не актуален, а CoC и HoTT я реализовал, и куда важнее кубическую теорию дальше (успеть) сделать -- чётко под задачи программиста-миддла. Хотя бы научить рассуждать in small в соответствующих моделях. Например, цепочка конвертации данных с помощью унивалентности (композиция путей соответствует композиции эквивалентностей) с автоматическим доказательством коммутативности преобразований. И постепенно выходим на уровень формального мышления in large.
А без понимания теории типов все проекты будут получаться как на картинке,
но я уже совсем один остался в России в этих темках куда-то ещё едва бреду.....
все уснули давно
в километрах глубин
никого ничего он остался один....
кто сказал что нельзя
переплыть океан
это грустная шутка это хитрый обман...
я сумею доплыть
под сияние звёзд
я хочу увидать край где много берёз...
4👍53❤🔥9✍4😁4🤔2
Преподы мехмата рассказывают, что студенты там сходят с ума по нейронкам, хорошо ещё что по математике внутрянки, но всё равно на выходе 98% это говнопроекты с вайб-кодингом, от которых больше вреда чем пользы, и зарплаты так себе.
А вот на формальные темы, верификацию, теорию типов, студента и на аркане не затащишь, хотя это абсолютно критичные темы для тех самых 2% критически важных инфраструктур.
...есть один русскоязычный полуживой чятик по формальным методам, где админ с поехавший кукухой (сам так говорит), 50% работают в европейских профильных структурах типа INRIA (потому что европейская школа computer science абсолютный топчик, Америка сильно остаёт), а 48% мечтают туда свалить после PhD, для чего старательно выискивают подходящие темки, как бы опубликоваться в международных академических изданиях и засветиться на научных конфах.
При этом я даже лично знаю несколько человек, теперь уже полностью "с противоположной стороны баррикад", кто их старательно и успешно к себе сманивает.
Ну и изучают они соответственно западные теорем-пруверы вроде Rocq и англоязычные гайды, и ни о каком развитии этой темки в России конечно речь уже давно не идёт, это я как-то ещё шевелюсь...
...И о медалях-орденах ты помышлять не моги:
Всего награды -- только знать наперёд,
Что по весне споткнётся кто-то о твои сапоги
И идиотский твой штандарт подберёт.
А вот на формальные темы, верификацию, теорию типов, студента и на аркане не затащишь, хотя это абсолютно критичные темы для тех самых 2% критически важных инфраструктур.
...есть один русскоязычный полуживой чятик по формальным методам, где админ с поехавший кукухой (сам так говорит), 50% работают в европейских профильных структурах типа INRIA (потому что европейская школа computer science абсолютный топчик, Америка сильно остаёт), а 48% мечтают туда свалить после PhD, для чего старательно выискивают подходящие темки, как бы опубликоваться в международных академических изданиях и засветиться на научных конфах.
При этом я даже лично знаю несколько человек, теперь уже полностью "с противоположной стороны баррикад", кто их старательно и успешно к себе сманивает.
Ну и изучают они соответственно западные теорем-пруверы вроде Rocq и англоязычные гайды, и ни о каком развитии этой темки в России конечно речь уже давно не идёт, это я как-то ещё шевелюсь...
...И о медалях-орденах ты помышлять не моги:
Всего награды -- только знать наперёд,
Что по весне споткнётся кто-то о твои сапоги
И идиотский твой штандарт подберёт.
2👍53🤔11💯8🔥3😁2
Прекрасное: разработка, управляемая мазохизмом.
A masochist’s guide to web development
Пишем веб-приложение на сишечке и wasm.
emnoscripten, колбеки между си/js, многопоточность в браузере, persistent storage через idbfs... Элегантная фишка: вынос тяжёлых вычислений в веб-воркер.
A masochist’s guide to web development
Пишем веб-приложение на сишечке и wasm.
emnoscripten, колбеки между си/js, многопоточность в браузере, persistent storage через idbfs... Элегантная фишка: вынос тяжёлых вычислений в веб-воркер.
👍34😁19✍10🎉1🤓1
2. Однажды Бобрик пришёл к старому БоброМудру и спросил:
-- Учитель! А если бы появилась теория типов ещё более сложная, чем HoTT и CoC, вы бы смогли и её реализовать?
-- Без проблем, - ответил БоброМудр.
-- Но как?? - изумился Бобрик.
-- А вот так! - ответил БоброМудр, и дал Бобрику подзатыльник.
-- Учитель! А если бы появилась теория типов ещё более сложная, чем HoTT и CoC, вы бы смогли и её реализовать?
-- Без проблем, - ответил БоброМудр.
-- Но как?? - изумился Бобрик.
-- А вот так! - ответил БоброМудр, и дал Бобрику подзатыльник.
1😁62🫡2🤯1
Вчера решил обновить Нах, кнопочкой (сам он не умеет проверять апдейты), и он скачивает и запускает из самого себя полностью автономный инсталлятор. Окошечко с кнопкой скачивания, выбор каталога, весь UI -- какой-то древний стиль Delphi из 2000-х.
Так как инсталлятор автономный то он по определению не способен выбрать каталог установки, где уже размещается Нах; предлагает стандартный c: program files, тоже приходится ручками задавать,
И после чего это чудо ничтоже сумняшеся начинает установку при непосредственно работающем экземпляре Наха, ну и естественно возникает классическая проблема ↑↑↑
(Сделать инсталлятор, автоматически определяющий обновления и умеющий полноценно перезаписывать свою копию при новом апдейте -- это уровень лабораторной работы первого курса на пару часов.)
Детский сад какой-то, ей-богу.
За $1m мои ментаты сделают абсолютно защищённый и формально верифицированный мессенджер уровня телеграма (чаты + продвинутая ai-система рекомендации каналов) на 100 млн пользователей и миллион rps.
Но это в теории, на практике никому не рекомендую связываться с госконтрактами: по итогу сами останетесь много должны, и будете ещё благодарить что не упрятали в кутузку.
Уж лучше, честное слово, чем браться за что-то подобное, лучше заниматься иллюзорным стартаперством =>
"...Последние 3 недели был в Долине: полсотни встреч с стартапами и фондами, организация двух конференций, участие в пяти, два хакатона и куча эмоций.
...В городе не осталось ни одного билборда, который бы рекламировал что-то кроме ИИ. Энергия через край. Я уже писал, что в воскресенье вечером в кафе нет свободного стула, потому что все кодят стартапы. Уровень общего воодушевления выше, чем когда-либо на моей памяти."
А на моей памяти практически точно такое же было в конце девяностых, когда только зарождался тот самый "пузырь доткомов", а потом в 2000-е "пузырь shareware" и т.д. Тогда просто не было доступных ноутбуков, поэтому сидели все за домашними компами 🤓
Так как инсталлятор автономный то он по определению не способен выбрать каталог установки, где уже размещается Нах; предлагает стандартный c: program files, тоже приходится ручками задавать,
И после чего это чудо ничтоже сумняшеся начинает установку при непосредственно работающем экземпляре Наха, ну и естественно возникает классическая проблема ↑↑↑
(Сделать инсталлятор, автоматически определяющий обновления и умеющий полноценно перезаписывать свою копию при новом апдейте -- это уровень лабораторной работы первого курса на пару часов.)
Детский сад какой-то, ей-богу.
За $1m мои ментаты сделают абсолютно защищённый и формально верифицированный мессенджер уровня телеграма (чаты + продвинутая ai-система рекомендации каналов) на 100 млн пользователей и миллион rps.
Но это в теории, на практике никому не рекомендую связываться с госконтрактами: по итогу сами останетесь много должны, и будете ещё благодарить что не упрятали в кутузку.
Уж лучше, честное слово, чем браться за что-то подобное, лучше заниматься иллюзорным стартаперством =>
"...Последние 3 недели был в Долине: полсотни встреч с стартапами и фондами, организация двух конференций, участие в пяти, два хакатона и куча эмоций.
...В городе не осталось ни одного билборда, который бы рекламировал что-то кроме ИИ. Энергия через край. Я уже писал, что в воскресенье вечером в кафе нет свободного стула, потому что все кодят стартапы. Уровень общего воодушевления выше, чем когда-либо на моей памяти."
А на моей памяти практически точно такое же было в конце девяностых, когда только зарождался тот самый "пузырь доткомов", а потом в 2000-е "пузырь shareware" и т.д. Тогда просто не было доступных ноутбуков, поэтому сидели все за домашними компами 🤓
👍43😁13💯4🤔3🤓1
Закачиваю гайд по Calculus of Constructions, много читаю по теме, вот свежачок "Programs as Singularities" университета Мельбурна.
Канадцы пытаются связать дискретный мир программ и доказательств с непрерывным миром машинного обучения через алгебраическую геометрию.
Исторически концепция алгоритма/программы развивалась из двух направлений:
- логические рассуждения (от Аристотеля)
- алгебраические вычисления (от аль-Хорезми)
Сегодня концептуальный ландшафт впервые за всю историю кибернетикэ качественно меняется: скоро большая часть сложных когнитивных процессов будет происходить "в машинах".
Авторы пытаются "встроить" дискретный мир программ в непрерывный мир машинного обучения. Но это должно быть гомоморфное отображение: внутренняя структура программ должна отражаться в геометрической структуре непрерывного пространства. Любая наша программа - это набор дискретных инструкций, но нейросети работают в непрерывном пространстве (с вероятностями, градиентами), а программы - в дискретном (чёткие инструкции). И как это состыковать?
Авторы предлагают т.н. "структурный байесианизм".
Программа отображается в "особую" точку (сингулярность, где potential function имеет особое поведение). Структура программы отражается в геометрии пространства вокруг этой точки, а ошибки соответствуют определённым типам деформаций около сингулярности. В результате AI сможет "понимать" программы не как черный ящик, а через их геометрическую структуру. Люди (топологи) смогут оценивать "красоту" и эффективность внутренней структуры модели буквально эстетическим чувством, а система сможет "видеть" структуру ошибки геометрически и находить ближайшее корректное решение в этом пространстве.
Таким образом формируется математический мост между классическим программированием и машинным обучением.
Но подход авторов нацелен конкретно на ML, и ему не хватает ни глубины, ни универсальности, ни прагматизма. Правильно это конечно делать в парадигме гомотопической теории, где геометрия проявляется через непрерывные деформации (гомотопии). HoTT уже имеет хорошо развитый аппарат для работы с непрерывными деформациями типов, понятие type identity естественно связывается с геометрической структурой, а формализовать переход между дискретным и непрерывным могут высшие индуктивные типы.
Например, алгоритм сортировки может быть представлен как зависимый тип
Определяем пространство всех возможных программ заданного типа.
Разные реализации одного алгоритма становятся путями в этом пространстве.
Оптимизация нейросети - непрерывное движение по этому пространству.
Можно доказывать корректность программ, можно определять "расстояние" между программами, можно плавно трансформировать одну программу в другую (на уровне AST) и т.д. и т.п.
Веса нейросети = точка в пространстве программ
Обучение = путь в этом пространстве
Ошибки = особые точки (сингулярности)
Таким образом получится формально доказывать свойства нейросетей, сам процесс их обучения становится непрерывным, а для анализа пространства решений используем топологические методы + визуализацию для человечков.
Основная проблема сейчас -- это исключительно разрыв между теоретической красотой HoTT и практическими инструментами для её применения в реальных задачах (такими, как у меня, но "я их вам не отдам, потому что у меня велосипеда нету" (с) Печкин :). Можно пытаться использовать кривейшие европейские теорем-пруверы, но у нас это зашквар, да и прошлый век уже.
Глубокоуважаемый AGIRu, забашляй $1m, и мы с пацанами такое сделаем.
Канадцы пытаются связать дискретный мир программ и доказательств с непрерывным миром машинного обучения через алгебраическую геометрию.
Исторически концепция алгоритма/программы развивалась из двух направлений:
- логические рассуждения (от Аристотеля)
- алгебраические вычисления (от аль-Хорезми)
Сегодня концептуальный ландшафт впервые за всю историю кибернетикэ качественно меняется: скоро большая часть сложных когнитивных процессов будет происходить "в машинах".
Авторы пытаются "встроить" дискретный мир программ в непрерывный мир машинного обучения. Но это должно быть гомоморфное отображение: внутренняя структура программ должна отражаться в геометрической структуре непрерывного пространства. Любая наша программа - это набор дискретных инструкций, но нейросети работают в непрерывном пространстве (с вероятностями, градиентами), а программы - в дискретном (чёткие инструкции). И как это состыковать?
Авторы предлагают т.н. "структурный байесианизм".
Программа отображается в "особую" точку (сингулярность, где potential function имеет особое поведение). Структура программы отражается в геометрии пространства вокруг этой точки, а ошибки соответствуют определённым типам деформаций около сингулярности. В результате AI сможет "понимать" программы не как черный ящик, а через их геометрическую структуру. Люди (топологи) смогут оценивать "красоту" и эффективность внутренней структуры модели буквально эстетическим чувством, а система сможет "видеть" структуру ошибки геометрически и находить ближайшее корректное решение в этом пространстве.
Таким образом формируется математический мост между классическим программированием и машинным обучением.
Но подход авторов нацелен конкретно на ML, и ему не хватает ни глубины, ни универсальности, ни прагматизма. Правильно это конечно делать в парадигме гомотопической теории, где геометрия проявляется через непрерывные деформации (гомотопии). HoTT уже имеет хорошо развитый аппарат для работы с непрерывными деформациями типов, понятие type identity естественно связывается с геометрической структурой, а формализовать переход между дискретным и непрерывным могут высшие индуктивные типы.
Например, алгоритм сортировки может быть представлен как зависимый тип
Sort : (A: Type) → (List A) → (List A) с доказательством упорядоченности, а нейросеть можно представить как тип NeuralNet : (Input: Type) → (Output: Type) → TypeОпределяем пространство всех возможных программ заданного типа.
Разные реализации одного алгоритма становятся путями в этом пространстве.
Оптимизация нейросети - непрерывное движение по этому пространству.
Можно доказывать корректность программ, можно определять "расстояние" между программами, можно плавно трансформировать одну программу в другую (на уровне AST) и т.д. и т.п.
Веса нейросети = точка в пространстве программ
Обучение = путь в этом пространстве
Ошибки = особые точки (сингулярности)
Таким образом получится формально доказывать свойства нейросетей, сам процесс их обучения становится непрерывным, а для анализа пространства решений используем топологические методы + визуализацию для человечков.
Основная проблема сейчас -- это исключительно разрыв между теоретической красотой HoTT и практическими инструментами для её применения в реальных задачах (такими, как у меня, но "я их вам не отдам, потому что у меня велосипеда нету" (с) Печкин :). Можно пытаться использовать кривейшие европейские теорем-пруверы, но у нас это зашквар, да и прошлый век уже.
Глубокоуважаемый AGIRu, забашляй $1m, и мы с пацанами такое сделаем.
1❤37😁10👍6🤯6✍3
Как умер мир музыки в целом (и рок в частности) с появлением интернета.
Hanson и Imagine Dragons сегодня встали в один ряд с Rolling Stones и Led Zeppelin...
Hanson и Imagine Dragons сегодня встали в один ряд с Rolling Stones и Led Zeppelin...
😁37🫡14👍7🤯2
...И всё же мой самый-самый любимый язык - это сишечка. Ну во-первых это самый массовый в мире функциональный язык программирования: в Си есть только функции, а структуры данных можно передавать по значению 🤓
Во-вторых, если серьёзно, на самом деле вы программируете на чистом функциональном языке препроцессора cpp (не путаем с c++ конечно), который состоит только из nestable expressions, которые не выполняются а оцениваются, и yields чистое значение типа Си, которое есть абстрактный тип данных (реализованный как char*). Затем это значение типа Си уже выполняется рантаймом (рантаймом cpp!), который обычно включает оптимизирующий генератор кода.
Преподобные гении Керниган и Ричи применили монады из теорката к разработке языков программирования значительно раньше, чем все остальные. Им пришлось немного прогнуться под антитеоретические штуки наподобие # undef, и правила определения области действия получились не так чисты, как, скажем, в лямбда-исчислении или Scheme (но, подождите, даже Джон Маккарти неправильно определил область действия в Лиспе.)
Следующим функциональным языком такого уровня стал Хаскель, где тип Си был сделан абстрактным ("IO"), хотя его всячески портили сектанты-вероотступники Черч, Карри и Милнер,
пока святой Wadler не допилил его до теоретически почти идеального... но по сути он остался не более чистым функциональным, чем Си + cpp.
Поэтому если хотите функциональности + мощнейшей экосистемы, пишите либо на Си под Линукс, либо на F# под .NET.
И забудьте про Java.
Во-вторых, если серьёзно, на самом деле вы программируете на чистом функциональном языке препроцессора cpp (не путаем с c++ конечно), который состоит только из nestable expressions, которые не выполняются а оцениваются, и yields чистое значение типа Си, которое есть абстрактный тип данных (реализованный как char*). Затем это значение типа Си уже выполняется рантаймом (рантаймом cpp!), который обычно включает оптимизирующий генератор кода.
Преподобные гении Керниган и Ричи применили монады из теорката к разработке языков программирования значительно раньше, чем все остальные. Им пришлось немного прогнуться под антитеоретические штуки наподобие # undef, и правила определения области действия получились не так чисты, как, скажем, в лямбда-исчислении или Scheme (но, подождите, даже Джон Маккарти неправильно определил область действия в Лиспе.)
Следующим функциональным языком такого уровня стал Хаскель, где тип Си был сделан абстрактным ("IO"), хотя его всячески портили сектанты-вероотступники Черч, Карри и Милнер,
пока святой Wadler не допилил его до теоретически почти идеального... но по сути он остался не более чистым функциональным, чем Си + cpp.
Поэтому если хотите функциональности + мощнейшей экосистемы, пишите либо на Си под Линукс, либо на F# под .NET.
И забудьте про Java.
3✍54😁10💯9❤4🐳2
.
Облако драгоценностей за неделю.
Основной паблик:
Разбираемся на практике, почему слабое связывание (loose coupling) — это ПЛОХО (в 100% учебников, курсов, университетов вас учат ровно противоположному: loose coupling — это ХОРОШО).
Засада с валидацией
Предыдущие серии:
Засада с микросервисами
Засада с исключениями
Засада с инициализацией
Засада с контроллером
Для донов-начинающих:
Мне кажется, что ещё чуть-чуть, и продавцов курсов "за полгода на работу, зп начинающего 70,000 рублей" начнут подкарауливать на улице их клиенты...
Как только вы освоите универсальные основы разработки, создание 99% программных систем действительно станет для вас довольно простым делом. Причина в том, что всё в разработке софта сводится к трем очень специфическим вещам: [...].
...Я говорю это для того, чтобы придать вам уверенности: чтобы добиться успеха в качестве разработчика, вам просто нужно по-настоящему овладеть тремя мета-навыками ↑↑↑
Для донов-неначинающих:
СильныеИдеи++
42. SOLID25 : [3...]
В заключение темы SOLID разбираем новую инженерную парадигму ей на смену, состоящую также из пяти принципов.
Почему умные люди невероятно тупы, и как вырваться из такой ловушки.
...В рамках такой модели достаточно хорошо получается описать гениальное мышление: большинство жизненных конфликтов или "неразрешимых" проблем возникают из-за того, что люди действуют на разных уровнях.
=
Напомню, что первые две дюжины существенно переработанных и улучшенных материалов СильныхИдей (по сути две книги) пока доступны на бусти, но скоро будет мощный третий гайд по SOLID, и дружелюбные цены вырастут:
1. БАЗА программной инженерии
2. Software Design с акцентом на Programming in Small
=
Новые материалы для ментатов Лаборатории.
В раздел "Элитный программист" добавлен материал
70) Шиза для программиста - 4.
В СильныеИдеи добавлен материал "120) Нечистый эффект наблюдения чистых функций".
В функциональной архитектуре (даже просто на уровне in small) чистые функции не могут выполнять "нечистые" действия. С другой стороны, наблюдение за результатом чистого вычисления будет побочным эффектом.
=
"Кубическая теория типов для программистов",
этим летом/осенью 💯 гайд будет готов.
Гайд по "Calculus of (Inductive) Constructions",
этим летом 💯 будет готов.
Контент весь я сделал, осталось отформатировать для библиотечного сервера, на неделе закончу.
Главный приятный вывод от погружения в CoC / CIC — что она сильно ограничена узким диапазоном задач (доказательства теорем и корректности программ, верификация свойств, автоматический вывод доказательств...), на что заточены все эти европейские пруверы Coq, Agda, Idris, Lean, которым обучают всю Европу и США — и за пределы CoC они выйти не могут, чтобы стать хотя бы немного ближе к ИТ.
Поэтому как закончу "кубики", берусь за разработку думательных паттернов (мантр) in large в парадигме гомотопической теории (переводим в неё software и system design сколько получится). Ну например простейшее - вместо
"внешний ключ связывает таблицы" мы можем думать об эквивалентности путей между типами данных, выявляя некорректные или избыточные связи ещё на этапе проектирования; составные ключи — это типы h-уровней (формальный способ рассуждать о разных уровнях уникальности данных и их отношениях);
с помощью высшего индуктивного типа Pushout корректно склеиваем разные типы (результат слияния таблиц будет консистентным независимо от порядка операций) и т.д. и т.п.
Ну и сам hott-кодинг конечно (абсолютный на сегодня уровень абстракций).
=
Self-Hack (тайм-менеджер + мотиватор + idle-игра).
Готово 25 уровней из ~50 альфа-версии,
этим летом бета-версия 💯 будет готова.
Босс 70-й лвл:
Полулегендарный самообучающийся алгоритм, управляющий крупнейшим в подполье крипто-миксером и сетью обналичивания. Не человек, а цифровая гидра с тройной системой защиты (блокчейн-лабиринт, изменчивые протоколы, физические серверы-призраки). Инициирует DDoS на твои кошельки и инструменты, насылает кибер-коллекторов, манипулирует курсами крипты на черных биржах, чтобы обесценить твои накопления...
Облако драгоценностей за неделю.
Основной паблик:
Разбираемся на практике, почему слабое связывание (loose coupling) — это ПЛОХО (в 100% учебников, курсов, университетов вас учат ровно противоположному: loose coupling — это ХОРОШО).
Засада с валидацией
Предыдущие серии:
Засада с микросервисами
Засада с исключениями
Засада с инициализацией
Засада с контроллером
Для донов-начинающих:
Мне кажется, что ещё чуть-чуть, и продавцов курсов "за полгода на работу, зп начинающего 70,000 рублей" начнут подкарауливать на улице их клиенты...
Как только вы освоите универсальные основы разработки, создание 99% программных систем действительно станет для вас довольно простым делом. Причина в том, что всё в разработке софта сводится к трем очень специфическим вещам: [...].
...Я говорю это для того, чтобы придать вам уверенности: чтобы добиться успеха в качестве разработчика, вам просто нужно по-настоящему овладеть тремя мета-навыками ↑↑↑
Для донов-неначинающих:
СильныеИдеи++
42. SOLID25 : [3...]
В заключение темы SOLID разбираем новую инженерную парадигму ей на смену, состоящую также из пяти принципов.
Почему умные люди невероятно тупы, и как вырваться из такой ловушки.
...В рамках такой модели достаточно хорошо получается описать гениальное мышление: большинство жизненных конфликтов или "неразрешимых" проблем возникают из-за того, что люди действуют на разных уровнях.
=
Напомню, что первые две дюжины существенно переработанных и улучшенных материалов СильныхИдей (по сути две книги) пока доступны на бусти, но скоро будет мощный третий гайд по SOLID, и дружелюбные цены вырастут:
1. БАЗА программной инженерии
2. Software Design с акцентом на Programming in Small
=
Новые материалы для ментатов Лаборатории.
В раздел "Элитный программист" добавлен материал
70) Шиза для программиста - 4.
В СильныеИдеи добавлен материал "120) Нечистый эффект наблюдения чистых функций".
В функциональной архитектуре (даже просто на уровне in small) чистые функции не могут выполнять "нечистые" действия. С другой стороны, наблюдение за результатом чистого вычисления будет побочным эффектом.
=
"Кубическая теория типов для программистов",
этим летом/осенью 💯 гайд будет готов.
Гайд по "Calculus of (Inductive) Constructions",
этим летом 💯 будет готов.
Контент весь я сделал, осталось отформатировать для библиотечного сервера, на неделе закончу.
Главный приятный вывод от погружения в CoC / CIC — что она сильно ограничена узким диапазоном задач (доказательства теорем и корректности программ, верификация свойств, автоматический вывод доказательств...), на что заточены все эти европейские пруверы Coq, Agda, Idris, Lean, которым обучают всю Европу и США — и за пределы CoC они выйти не могут, чтобы стать хотя бы немного ближе к ИТ.
Поэтому как закончу "кубики", берусь за разработку думательных паттернов (мантр) in large в парадигме гомотопической теории (переводим в неё software и system design сколько получится). Ну например простейшее - вместо
"внешний ключ связывает таблицы" мы можем думать об эквивалентности путей между типами данных, выявляя некорректные или избыточные связи ещё на этапе проектирования; составные ключи — это типы h-уровней (формальный способ рассуждать о разных уровнях уникальности данных и их отношениях);
с помощью высшего индуктивного типа Pushout корректно склеиваем разные типы (результат слияния таблиц будет консистентным независимо от порядка операций) и т.д. и т.п.
Ну и сам hott-кодинг конечно (абсолютный на сегодня уровень абстракций).
=
Self-Hack (тайм-менеджер + мотиватор + idle-игра).
Готово 25 уровней из ~50 альфа-версии,
этим летом бета-версия 💯 будет готова.
Босс 70-й лвл:
Полулегендарный самообучающийся алгоритм, управляющий крупнейшим в подполье крипто-миксером и сетью обналичивания. Не человек, а цифровая гидра с тройной системой защиты (блокчейн-лабиринт, изменчивые протоколы, физические серверы-призраки). Инициирует DDoS на твои кошельки и инструменты, насылает кибер-коллекторов, манипулирует курсами крипты на черных биржах, чтобы обесценить твои накопления...
3👍43⚡9😁5
Я закончил таки кубическую теорию (всего за 200 долларов на клода4) , было очень тяжело, местами несколько раз даже думал что вообще не справлюсь. Засада в том что подтянуть готовую реализацию из HoTT не получается, кубики это по сути самостоятельная теория типов, и в итоге пришлось делать её полностью с нуля. Но с другой стороны это и хорошо.
Базовые структуры для работы с кубами (Interval, Direction, Face, Cube, System); механизмы для работы с путями и транспортом типов; реализация эквивалентностей и унивалентности, базовые Higher Inductive Types.
Кубические пути позволяют формально описывать и проверять трансформации между типами данных. Транспорт типов (CubicalTransport) обеспечивает безопасную миграцию данных при изменении структуры типов. Эквивалентности (CubicalEquivalence) гарантируют сохранение свойств при рефакторинге.
N-мерные кубы (Cube) естественно моделируют пространство состояний параллельных процессов. Система правил (System) позволяет описывать допустимые переходы между состояниями. Композиция Кана (Kan composition) обеспечивает корректное слияние параллельных изменений.
Higher Inductive Types позволяют определять абстрактные типы данных с встроенными инвариантами. Пути (CubicalPath) формализуют допустимые преобразования данных.
Унивалентность (Univalence) обеспечивает перенос свойств между эквивалентными представлениями -- она становится вычислимым свойством (реализуется transport типов), а не просто аксиомой, как в HoTT, что делает CTT более практичной.
И теперь у меня полный комплект: HoTT, CoC, CTT.
Базовые структуры для работы с кубами (Interval, Direction, Face, Cube, System); механизмы для работы с путями и транспортом типов; реализация эквивалентностей и унивалентности, базовые Higher Inductive Types.
Кубические пути позволяют формально описывать и проверять трансформации между типами данных. Транспорт типов (CubicalTransport) обеспечивает безопасную миграцию данных при изменении структуры типов. Эквивалентности (CubicalEquivalence) гарантируют сохранение свойств при рефакторинге.
N-мерные кубы (Cube) естественно моделируют пространство состояний параллельных процессов. Система правил (System) позволяет описывать допустимые переходы между состояниями. Композиция Кана (Kan composition) обеспечивает корректное слияние параллельных изменений.
Higher Inductive Types позволяют определять абстрактные типы данных с встроенными инвариантами. Пути (CubicalPath) формализуют допустимые преобразования данных.
Унивалентность (Univalence) обеспечивает перенос свойств между эквивалентными представлениями -- она становится вычислимым свойством (реализуется transport типов), а не просто аксиомой, как в HoTT, что делает CTT более практичной.
И теперь у меня полный комплект: HoTT, CoC, CTT.
2🤯40🏆14✍7🔥2😁2
Соответственно теперь отформатирую весь контент по кубикам в гайд для библиотечного сервера, и дальше берусь за думательные паттерны в этих теориях.
Кубики в целом более интуитивная модель для программистов (кубы vs абстрактные пути) + прямая связь с параллельным программированием, Но для меня важнее сила абстракций, а она топчик в гомотопической теории конечно.
CTT:
Явно моделируем переходы и трансформации.
Получаем формальные гарантии корректности через композицию путей.
Можем проанализировать (например с помощью солвера Z3) все комбинации состояний.
Чётко видим и понимаем инварианты на гранях куба.
=
Ну вот совсем примитивная "кубическая" метафора которую вы можете использовать прямо сейчас.
Безопасные миграции с сохранением истории.
Отслеживание состояний валидации.
Возможность отката изменений.
Или вот:
Управление распределённой согласованностью.
Адаптивные уровни гарантий для разных типов.
Безопасные преобразования между представлениями.
=
Вы это всё прочитали и подумали про себя "мне всё понятно! буду такие же кубики делать!". Это - 💯 признак что вам вообще ничего не понятно. Предлагаю тогда - возьмите жпт и разберите самостоятельно. Вы наверняка умнее меня и сами всё знаете.Хотя я так не думаю.
Кубики в целом более интуитивная модель для программистов (кубы vs абстрактные пути) + прямая связь с параллельным программированием, Но для меня важнее сила абстракций, а она топчик в гомотопической теории конечно.
CTT:
Явно моделируем переходы и трансформации.
Получаем формальные гарантии корректности через композицию путей.
Можем проанализировать (например с помощью солвера Z3) все комбинации состояний.
Чётко видим и понимаем инварианты на гранях куба.
=
Ну вот совсем примитивная "кубическая" метафора которую вы можете использовать прямо сейчас.
Измерения куба:
- Ось X: Версии схемы данных (0 -> 1)
- Ось Y: Состояния данных (валидное -> невалидное)
- Ось Z: Время (t0 -> t1)
Грани куба (Face):
- (X=0): Старая схема
- (X=1): Новая схема
- (Y=0): Валидные данные
- (Y=1): Временно невалидные
- (Z=0): Начальное время
- (Z=1): Конечное время
Пути (CubicalPath):
- Миграция: путь по X (схема -> схема)
- Валидация: путь по Y (невалидное -> валидное)
- История: путь по Z (время -> время)
Безопасные миграции с сохранением истории.
Отслеживание состояний валидации.
Возможность отката изменений.
Или вот:
Измерения куба:
- Ось X: Узлы распределенной БД (node1 -> node2)
- Ось Y: Уровни согласованности (eventual -> strong)
- Ось Z: Типы данных (simple -> complex)
Грани:
- (X=0,1): Состояния узлов
- (Y=0,1): Гарантии согласованности
- (Z=0,1): Структуры данных
Пути:
- Репликация: путь между узлами
- Усиление согласованности: путь по Y
- Преобразование типов: путь по Z
Управление распределённой согласованностью.
Адаптивные уровни гарантий для разных типов.
Безопасные преобразования между представлениями.
=
Вы это всё прочитали и подумали про себя "мне всё понятно! буду такие же кубики делать!". Это - 💯 признак что вам вообще ничего не понятно. Предлагаю тогда - возьмите жпт и разберите самостоятельно. Вы наверняка умнее меня и сами всё знаете.
2👍35🤯25😁7⚡1🔥1
Продолжаю работу с ментатами 🤓
...На первый взгляд, это какой-то кошмар. Интересно было бы посмотреть на мир глазами человека, который создал вим, потому что подход к организации крайне нестандартный. Но часто слышала, что им пользуются коллеги и получают от этого какие-то бенефиты, придется поверить, что это со временем становится удобно.
...на работе активно пошли собесы и скрининги. Стараюсь сейчас задавать много новых вопросов, чтобы повторять/углублять старый и изучать новый материал. Без этой активности совсем грустно было: теория быстро выветривается, если ее активно не применяешь. А ходить на большое количество собеседований в качестве кандидата съедает много сил и времени + в целом не добиться такой же интенсивности.
...Продолжаю откликаться на вакансии в hh. На этот раз оставлял отклики пачками. Активность hr заметно выросла. Поговорил с hr'ами из трех компаний. Одни предложили ЗП для Senior/Lead в 350 т.р. :)), по второму жду ОС, третьи (аутстаф) сами предложили трудоустройство full-time трудоустройство параллельно с основным местом работы.
...Есть две проблемы:
- understaff
- идиоты в платформе, которые ничего не могут без меня сделать. Хорошо если бы они просто не могли, так они ломают все.
...А сегодня сели чинить, оказалось последний бекап лежит за ноябрь 2024 года.
...Дополнительно, впервые увидел базы данных такого масштаба, понимаю что в реальных проектах все гораздо сложнее. Действительно, проектировщики баз данных не зря выделены в отдельное направление.
...И вот буквально вчера тимлид сказал, что было бы неплохо накидать базовый веб-интерфейс для взаимодействия с проектом, за который я отвечаю. Интерфейс нужен для разработчиков, чтобы просто заглянуть что лежит в таблицах в БД.
Получается, что я удачно решил писать дипломный проект. Да и я прямо чувствую, как закрываются некоторые пробелы благодаря диплому.
...У меня такое ощущение, что у меня в голове сжимается некая пружина, и когда придёт время погружаться в новый проект на новой работе, я удивлюсь, как быстро в моей голове начинает укладываться архитектура того, с чем я работаю.
...Вернулся из оптуска, нифига не отдохнул (семья)
...Задач писать новый код на сотни строк пока совсем нет
...Затем позвали на финал с тимлидом. Не сразу нашли контакт, но в итоге оффер на 500 т.р. после вычета налогов получил. Сначала просил 450 и.р., но сторговаться).... Но у меня на текущем месте больше зп, поэтому сижу ровно :)
=
Я это запостил, потому что вам нравится такое читать.
Но вот что вам не нравится читать: более полугода 2025 уже прошло, а насколько выросла за этот период твоя зарплата? На какие-нибудь жалкие 10%, в разы меньше реальной инфляции? Если выросла вообще.
Вам менеджер(ка) промычал(а) на ваш запрос: нууууу я спрошу у рукоммводсммтва насчёт уууу повышения но у нас строгие грээээйды , а сейчас и проблемы с финансами бооооольшие...
Вы считаете это нормальным? Когда взрослый здоровый мужик ждёт, что кто-то будет за него бегать и выпрашивать "подбросить немного деньжат" для его семьи? Вы можете сейчас каждый день покупать свежую черешню и клубнику для своих детей?
...На первый взгляд, это какой-то кошмар. Интересно было бы посмотреть на мир глазами человека, который создал вим, потому что подход к организации крайне нестандартный. Но часто слышала, что им пользуются коллеги и получают от этого какие-то бенефиты, придется поверить, что это со временем становится удобно.
...на работе активно пошли собесы и скрининги. Стараюсь сейчас задавать много новых вопросов, чтобы повторять/углублять старый и изучать новый материал. Без этой активности совсем грустно было: теория быстро выветривается, если ее активно не применяешь. А ходить на большое количество собеседований в качестве кандидата съедает много сил и времени + в целом не добиться такой же интенсивности.
...Продолжаю откликаться на вакансии в hh. На этот раз оставлял отклики пачками. Активность hr заметно выросла. Поговорил с hr'ами из трех компаний. Одни предложили ЗП для Senior/Lead в 350 т.р. :)), по второму жду ОС, третьи (аутстаф) сами предложили трудоустройство full-time трудоустройство параллельно с основным местом работы.
...Есть две проблемы:
- understaff
- идиоты в платформе, которые ничего не могут без меня сделать. Хорошо если бы они просто не могли, так они ломают все.
...А сегодня сели чинить, оказалось последний бекап лежит за ноябрь 2024 года.
...Дополнительно, впервые увидел базы данных такого масштаба, понимаю что в реальных проектах все гораздо сложнее. Действительно, проектировщики баз данных не зря выделены в отдельное направление.
...И вот буквально вчера тимлид сказал, что было бы неплохо накидать базовый веб-интерфейс для взаимодействия с проектом, за который я отвечаю. Интерфейс нужен для разработчиков, чтобы просто заглянуть что лежит в таблицах в БД.
Получается, что я удачно решил писать дипломный проект. Да и я прямо чувствую, как закрываются некоторые пробелы благодаря диплому.
...У меня такое ощущение, что у меня в голове сжимается некая пружина, и когда придёт время погружаться в новый проект на новой работе, я удивлюсь, как быстро в моей голове начинает укладываться архитектура того, с чем я работаю.
...Вернулся из оптуска, нифига не отдохнул (семья)
...Задач писать новый код на сотни строк пока совсем нет
...Затем позвали на финал с тимлидом. Не сразу нашли контакт, но в итоге оффер на 500 т.р. после вычета налогов получил. Сначала просил 450 и.р., но сторговаться).... Но у меня на текущем месте больше зп, поэтому сижу ровно :)
=
Я это запостил, потому что вам нравится такое читать.
Но вот что вам не нравится читать: более полугода 2025 уже прошло, а насколько выросла за этот период твоя зарплата? На какие-нибудь жалкие 10%, в разы меньше реальной инфляции? Если выросла вообще.
Вам менеджер(ка) промычал(а) на ваш запрос: нууууу я спрошу у рукоммводсммтва насчёт уууу повышения но у нас строгие грээээйды , а сейчас и проблемы с финансами бооооольшие...
Вы считаете это нормальным? Когда взрослый здоровый мужик ждёт, что кто-то будет за него бегать и выпрашивать "подбросить немного деньжат" для его семьи? Вы можете сейчас каждый день покупать свежую черешню и клубнику для своих детей?
2😁32👍18💯12❤7🫡1
Научный свежачок от Apple: The Illusion of Thinking: Understanding the Strengths and Limitations of Reasoning Models via the Lens of Problem Complexity.
Почему LRM-ки (это которые дипсинкинг) -- лишь инструменты для узких задач, а их "рассуждения" -- оптимизированная генерация, не способная к истинному обобщению. Прорыв потребует новых архитектур, а не масштабирования текущих подходов.
LRM далеки от AGI: их "мышление" поверхностно и не масштабируется. Они не могут строго следовать даже готовым алгоритмам. Бесполезная трата ресурсов после нахождения решения. Математические бенчмарки уязвимы для оптимизации: нужны наборы, где нельзя угадать паттерн.
Преимущество LRM в математических бенчмарках (AIME, MATH) -- артефакт контаминации данных. Их "рассуждения" -- оптимизация под среднюю сложность, а не обобщаемый навык. За порогом сложности LRM не просто ошибаются -- они отказываются от попыток решать (снижают усилия, хотя контекстное окно позволяет продолжать).
Нужны архитектуры, способные к последовательной верификации и алгоритмической строгости (например, кубическая теория типов).
Интересно, какие показательные тесты авторы подобрали -- пазлы.
Hanoi (экспоненциальная сложность), Checker Jumping (квадратичная), River Crossing/Blocks World (линейная) — покрывают нужный спектр тестов. Но в Tower of Hanoi LRM делают до 100 верных шагов, а в River Crossing ошибаются на 5-м шаге.
Рекомендую кстати поиграть в River Crossing.
Простые задачи: Раннее верное решение -- затем "перемудривание" (генерируют ошибки).
Средние задачи: Верное решение появляется позже после проб и ошибок. LRM тут проявляют преимущество над LLM за счёт "размышлений".
Сложные задачи: Нет верных решений в цепочке рассуждений. Полный коллапс всех моделей (точность -> 0%), несмотря на огромные вычислительные ресурсы.
Программисты, выдыхаем и идём неспешно разбираться в software design.
Почему LRM-ки (это которые дипсинкинг) -- лишь инструменты для узких задач, а их "рассуждения" -- оптимизированная генерация, не способная к истинному обобщению. Прорыв потребует новых архитектур, а не масштабирования текущих подходов.
LRM далеки от AGI: их "мышление" поверхностно и не масштабируется. Они не могут строго следовать даже готовым алгоритмам. Бесполезная трата ресурсов после нахождения решения. Математические бенчмарки уязвимы для оптимизации: нужны наборы, где нельзя угадать паттерн.
Преимущество LRM в математических бенчмарках (AIME, MATH) -- артефакт контаминации данных. Их "рассуждения" -- оптимизация под среднюю сложность, а не обобщаемый навык. За порогом сложности LRM не просто ошибаются -- они отказываются от попыток решать (снижают усилия, хотя контекстное окно позволяет продолжать).
Нужны архитектуры, способные к последовательной верификации и алгоритмической строгости (например, кубическая теория типов).
Интересно, какие показательные тесты авторы подобрали -- пазлы.
Hanoi (экспоненциальная сложность), Checker Jumping (квадратичная), River Crossing/Blocks World (линейная) — покрывают нужный спектр тестов. Но в Tower of Hanoi LRM делают до 100 верных шагов, а в River Crossing ошибаются на 5-м шаге.
Рекомендую кстати поиграть в River Crossing.
Простые задачи: Раннее верное решение -- затем "перемудривание" (генерируют ошибки).
Средние задачи: Верное решение появляется позже после проб и ошибок. LRM тут проявляют преимущество над LLM за счёт "размышлений".
Сложные задачи: Нет верных решений в цепочке рассуждений. Полный коллапс всех моделей (точность -> 0%), несмотря на огромные вычислительные ресурсы.
Программисты, выдыхаем и идём неспешно разбираться в software design.
2😁33👍16❤7✍7🤔2
.
Действительно умён тот, кто освятил и свой ум.
прп. Паисий Святогорец
Математика и музыка, литература и программный код - это т.н. антитовар. Это вещи, которые не истощаются при использовании или раздаче даром, а наоборот становятся всё больше и ценнее, как хлеб и рыба в Евангелии.
Акционеры и руководство любых современных соцсетей ведут себя так, как будто их корпоративные обязанности продиктованы дружбой и доброжелательностью -- они даже называют нас всех друзьями, точно так же, как в советские время обращались ко всем "товарищ". Но это всего лишь дымовая завеса для компании, построенной на зарабатывании денег, а не на обмене дарами. Это ещё хуже и гаже, чем развод пенсионеров "казначейством и прокурором по вотсапу"
Глубинное государство Сети -- это компании, которые притворяются, что дарят вам подарки. Не поддавайтесь.
Имея дело с любыми соцсетями и мессенджерами, мы должны быть ещё более подозрительными, чем при заключении сделок с рекрутером или риэлтором -- как из-за виртуального маскарада, так и из-за их огромной власти, которая приближается к монопольному уровню при безмолвной поддержке государством этого тотально лживого беспредела.
Прежде всего, мы должны требовать абсолютной прозрачности. Фарс с приглашением и без того нищих музыкантов для участия в фальшивом обмене талантливыми произведениями, в то время как миллиардеры обогащаются за счет своих нулевых усилий, должен называться тем, что он и есть на самом деле -- а именно инструментом капиталистической эксплуатации, причём в невиданных ранее масштабах.
Мы должны вызывать общественный резонанс, когда какой-либо онлайновый бизнес просит творческого профессионала работать бесплатно, "за лайки", просто выкладывая свою музыку, рисунки, видео. Это позорная практика, и к ней следует относиться как к таковой.
Мы должны уважать интеллектуальную собственность одарённых людей. Пока же соцсети только их уничтожают, фактически лишая нас возможности услышать истинно талантливых артистов, музыкантов и поэтов -- целителей уставших наших душ...
Но иногда одарённые люди действительно сопротивляются. Андеграунд жив.
Действительно умён тот, кто освятил и свой ум.
прп. Паисий Святогорец
Математика и музыка, литература и программный код - это т.н. антитовар. Это вещи, которые не истощаются при использовании или раздаче даром, а наоборот становятся всё больше и ценнее, как хлеб и рыба в Евангелии.
Акционеры и руководство любых современных соцсетей ведут себя так, как будто их корпоративные обязанности продиктованы дружбой и доброжелательностью -- они даже называют нас всех друзьями, точно так же, как в советские время обращались ко всем "товарищ". Но это всего лишь дымовая завеса для компании, построенной на зарабатывании денег, а не на обмене дарами. Это ещё хуже и гаже, чем развод пенсионеров "казначейством и прокурором по вотсапу"
Глубинное государство Сети -- это компании, которые притворяются, что дарят вам подарки. Не поддавайтесь.
Имея дело с любыми соцсетями и мессенджерами, мы должны быть ещё более подозрительными, чем при заключении сделок с рекрутером или риэлтором -- как из-за виртуального маскарада, так и из-за их огромной власти, которая приближается к монопольному уровню при безмолвной поддержке государством этого тотально лживого беспредела.
Прежде всего, мы должны требовать абсолютной прозрачности. Фарс с приглашением и без того нищих музыкантов для участия в фальшивом обмене талантливыми произведениями, в то время как миллиардеры обогащаются за счет своих нулевых усилий, должен называться тем, что он и есть на самом деле -- а именно инструментом капиталистической эксплуатации, причём в невиданных ранее масштабах.
Мы должны вызывать общественный резонанс, когда какой-либо онлайновый бизнес просит творческого профессионала работать бесплатно, "за лайки", просто выкладывая свою музыку, рисунки, видео. Это позорная практика, и к ней следует относиться как к таковой.
Мы должны уважать интеллектуальную собственность одарённых людей. Пока же соцсети только их уничтожают, фактически лишая нас возможности услышать истинно талантливых артистов, музыкантов и поэтов -- целителей уставших наших душ...
Но иногда одарённые люди действительно сопротивляются. Андеграунд жив.
1👍45🔥16❤🔥9❤4😁1
AI-IDE и абонемент в тренажёрный зал на грэпплинг -- это всё, что вам нужно (и одно из них необязательно) .
😁28❤19👍14🐳2🫡1