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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

❤️❤️❤️❤️❤️

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

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

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

Graviora manent.

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

Да, но...

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

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

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

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

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

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

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

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

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

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

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

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

=

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

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

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

=

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

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

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

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

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

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

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

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

(на картинке наша ламповая Лаборатория, РАЙцентр:)

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

Раз в месяц (вот как сегодня) я открываю одно место done на начальный тест "Годитесь ли вы в программисты". Кто его успешно проходит, может продолжить в моей Лаборатории. Но найти это место - хардкорный квест уровня хакерских паззлов из "Quadrilateral Cowboy" (правда, в прошлый раз его нашли за 15 минут :)


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

null

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

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

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

Продолжаю выкладывать для донов материалы СильныхИдей -- доступны моим ментатам, но тут расширенные версии, дополненные множеством примеров.
40. Жёсткий хейт SOLID (заключительное) : DIP
Dependency Inversion Principle — принцип инверсии зависимостей. Хотя в нём нету ничего принципиально неправильного, не будет преувеличением сказать, что тотальная одержимость инверсией зависимостей привела в 21-м веке к невосполнимым потерям на многие миллиарды долларов...

=

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


=

Новые материалы для ментатов-вычислителей.

В раздел "Элитный программист" добавлен материал
68) Как правильно планировать рабочий день.
Сколько помидорок в день лучше делать для оптимальной производительности и продуктивности? И вроде бы хочется сказать что это сильно зависит от человека... но нет.

... Гайд "Гомотопическая теория типов для программистов (2)": этим летом 💯 будет готов.
Фактически закончил, вычитываю (я вообще во всех своих материалах всегда очень тщательно выслеживаю всё что можно вплоть до идеальной пунктуации, всё форматирование делаю вручную, никаких html-редакторов) и выкладываю на библиотечный сервер. Получилось 57 топиков (в первом - 60).

По итогам двух гайдов: вся базовая теория HoTT смоделирована на питоне и покрыта тестами, приложены все исходники и тесты (никаких дополнительных библиотек кроме стандартных). Далее начинаю кубическую теорию .
По увлекательности и глубине с этим всем никакие шахматы или паззлы вроде baba is you и близко не сравнятся.
Ну или если угодно, это своеобразный gom-jabbar: он убивает только животных.

=

Трек "Чистое Проектирование/Software Design in Large", материал "Ясная архитектура"

null

=

На неделе немного отвлёкся на другой лабораторный проэкт self-hack: тайм-менеджер + мотиватор + idle-игра. У меня были маленькие самодельные программки под эти цели, которыми пользуюсь уже не один десяток лет, и зарекомендовали себя прекрасно, настало время зафиналить это всё, объединить лучшие подходы в одно. И беру также из игр наиболее аддиктивные фишечки, мотивирующие делать побольше помидорок в кайф.
Пока альфа-версия, 10% от беты; этим летом бета 💯 будет готова.
(код hand make 100%, ни капли ai)

idle — своеобразный тамагочи-хакер, сотни уровней.
Поиск и идентификация слабых сигналов в радиусе действия. Обнаружение открытых Wi-Fi точек, радионянь, дешевых смарт-замков, сигналов личных комов. Анализ базовых параметров (сила сигнала, тип шифрования, активность). Самодельный SDR модуль из хлама, антенна из пивной банки. Поиск халявного трафика в переполненных жилых блоках...
Босс: старый, параноидальный хакер-одиночка, десятилетиями контролирующий все значимые нелегальные частоты и пиратские ретрансляторы на районе. Его крепость - лабиринт из самодельных антенн и глушилок на крыше заброшенной промзоны. Его система - аналоговый кошмар, устойчивый к цифровым атакам...

(в далёких планах: pvp, блэкджеки и всё подобное.)

self-hack будет доступен БЕС-ПЛАТ-НО (но сперва для моих ментатов).

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

Уничтожьте их: запилите бесплатный SaaS-клон их основного платного сервиса, реализуйте за несколько часов 20% его оригинальных фишек, которые охватят 80% возможностей, и разово ливаните рекламу на 10 долларов на их клиентов (у компаний обычно есть свои группы в тг вк фб, вот туда...).

Ну и так-то, AI сегодня фактически уничтожил рынок SaaS-сервисов более чем полностью.

"Отдайте хоть данные, нелюди" (с)

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

Вот лучше чем ютуб блочить, сделали бы норм защиту от подобного. РосКомНадзирать-то легко, а вот где РосКомЗащита например?

Ну и как бы есть давно известные best practices для защиты от подобного.

Ладно, вот ещё одна: "НЕ называйте их best practices. Назовите их "известные более-менее хорошие практики".

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

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

p.s. 9 вечера: rusonyx всё лежит. поток комментов:
- Что со сроками восстановления? Деньги же теряем!
- Это уже зашквар, мы сваливаем с rusonix
- Ну пролежать почти весь рабочий день - ну круто, что я смогу сказать...
- Видимо, дела плохи. Поддержка ответила, что привлекли помощь

- Даже выдрать данные не получается пока что бы переехать к другому провайдеру(
(ну бэкапы-то всегда надо делать)

- Не у всех же на вашем хостинге копеечные сайты — конкретно нам суточный простой приносит убыток в среднем 1 миллион.
(ну а если и копеечные, их значит можно отрубать?:)

- Что за отношение к клиентам? Телефон не отвечает, на почту никто не отвечает. Сервера не работают, доступа нет. Что за зашквар? Нужно в офис приезжать? Отдайте хоть данные, нелюди

Интересно, а вдруг это не ддос, а вирус-шифровальщик? как в сдэке :)
Не волнуйтесь, у меня еженедельная копия всего сервера с базой на флешке.

p.p.s. 17-е утро: техподдержка: "всё плохо". русоникс убит? :)
РКН, спаси!!1

"...Наши инженеры продолжают работу над восстановлением нормальной работы сервисов, но указать приблизительные сроки решения проблемы не можем.
❗️Самое главное: сами серверы работают в штатном режиме, данные клиентов — в безопасности. Атака производится на сетевом уровне."
Ну а если вас будут ддосить бесконечно?

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

В любой непонятной ситуации делайте КОНТЕНТ, полезный другим. Вот и всё.

-- Но, Сергей Игоревич, посмотрите сколько вокруг контента, блогов, жпт, книг, гайдов, зачем, да и кому, нужен ещё один??

Вообще, на сегодня, уверен уже на 98%, остался единственный реальный путь создать соло итэ-бизнес с нуля -- это
a) вообще забыть про AI, и
b) развивать платный/донатный/рекламный блог, и/или вести условные "стримы за донаты". Подписчики -- это новая нефть.

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

=

Сейчас в Сеть хлещет какой-то бесконечный поток хипстерского жпт-кала, каждый день являются десятки новых ai-сервисов, доверие к которым уже стало фактически полным нулём. Ну и зачем пытаться влиться в эту муть? AI, позволивший создать кому угодно прототип чего угодно за один день, по сути уничтожил классическое стартаперство. То есть ровно как в сегодняшнем убитом найме: вместе с одним твоим честным резюме с тремя годами опыта на вакансию прилетает ещё 300 резюме с накруткой, и ты просто затеряешься.

=

Если бы я например начинал в какой-то новой темке с полного нуля, то первое бы что сделал -- это прошёл скучный качественный дорогой курс "Как зарабатывать на блоге", "Как развивать личный бренд" с проверенным ментором. Но и так тоже никто не делает.

Ну ok, на бусти за 1000 рублей можно найти отменные гайды по всем этим темам, им просто надо следовать. Но и так не хотят.

Напомню базу:
-- ваш блог - это по умолчанию готовый нетворк с кучей бонусов + потенциальные пользователи, ваших saas-ов :);
-- пока вы не зарабатываете на блоге миллион рублей в месяц, развивайте его исключительно через платную рекламу, и забудьте про органический трафик (вы бессмертный?);
-- вам надо взять одну (ОДНУ!) тему (в идеале -- вообще жёстко занишеваться), и тупо развивать её МИНИМУМ 9 месяцев.

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

А в англоязычном мире сабстэк например уже стал не просто средством заработка для отдельных известных блогеров, а по сути отдельной огромной экономикой, стилем жизни для множества профи, фактически одним из обязательных софт-скиллов. Поэтому если хотите создавать бизнес с нуля за доллары, изучайте как следует английский и идите на сабстэк; хотя я всё же посоветовал бы начинать с платного блога в России: если получится тут, то 100% получится и там, потому что там это во многом ми-ми-ми, а у нас это больше хардкор :)

=

За последние лет пять я читаю ну максимум дюжину русскоязычых программистских текстовых блогов в телеге/бусти, и примерно столько же видеоблогов на ютубе, которые хотя бы на 42% реально интересно почитать посмотреть. Причём из них примерно половина авторов живёт не в России.

И это ВСЁ. А потенциал русского рынка БЕСКОНЕЧЕН! И я, и многие другие, подписывались бы на хорошие платные блоги больше в разы, и на ютубе донатили бы на каждом стриме -- но их как не было, так и нету.

Я не знаю, почему так, честно.

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

Ну ок.

Пророческое от Пелевина (2011-й!), про промпты :)

"Священники говорят, что любое обращение к Сингулярному должно подробно излагать все обстоятельства дела. Злые языки уверяют – причина в накрутках за декламацию: чем длинее воззвание, тем дороже стоит зачитать его в храме."

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

Другое дело, что Клод вряд ли будет прямо точно этого всего придерживаться - примерно как в армии приказ отдан и считается абсолютным к выполнению, но в реальной жизни отнюдь не факт что он будет выполнен 😬