В заключение сериала про инструменты формальной верификации.

Да, вполне можно с ними поконкурировать, но для этого надо выстраивать серьёзный бизнес. Можно конечно делать верификацию и на 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 🚀 некоторые вещи конечно просто очевидны, именно поэтому их не замечаешь.

Заключительный пост сериала будет про это.