В течение последних двух лет я медленно, но верно продвигаюсь по этому пути. Изучив Rust несколько лет назад и начав серьезно использовать Typescript, я постепенно стал одержим типобезопасностью и крайне нетерпелив к коду, в котором есть легко предотвратимые баги и ошибки. Особенно в моей работе, где я был вынужден использовать python для создания крупных конвейеров данных. Меня очень раздражает, когда они падают после нескольких часов работы из-за специфических ошибок окружения, которые можно было бы быстро обнаружить с помощью проверки типов.

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

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

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

Получать обратную связь как можно раньше! Не закрывайте от мира ваши идеи.
Сначала реализуйте свою лучшую идею. Не тратьте время на то, что кажется "практичным", но на самом деле не является новаторскими. Лучше постепенно идти в направлении вашей лучшей идеи или подходить к ней со стороны, чем прятаться за теми, которые на самом деле неинтересны.
Обращайтесь за помощью! Мы добиваемся лучших результатов, когда находим других людей и кооперируемся с ними. Ваша полностью личная работа не впечатляет людей настолько, насколько вы думаете.

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

thin-ql: 09.02.2019-12.02.2020

GitHub - blainehansen/ts-thin-ql

github.com

Меня крайне раздражает объектно-реляционная проблематика. В течение многих лет я мечтал найти базу данных, которая имела бы сильные гарантии согласованности типа ACID, высокую производительность, сильно типизированные схемы и возможности целостности данных, а также объектно-графовый интерфейс запросов. Однако не было ничего лучше postgres, чтобы оправдать эти хлопоты, поэтому лучшее, что мне удалось найти, это проекты, которые просто предоставляют слой трансляции объектных графов поверх postgres, такие как postgrest и postgraphile. Эти проекты оба замечательные, и они в основном достаточно хороши, чтобы я был рад использовать их в работе. Postgraphile кажется отличным вариантом для практического веб-приложения, особенно в сочетании с генераторами из graphql в typescript.

Однако, когда я открыл для себя эти инструменты они не были настолько готовыми и у них была пара больших проблем, о которых я не мог просто забыть для многих своих проектов: они оба открывали полностью динамический API для всех внешних пользователей вместо компактного и они не были строго типизированными на всех уровнях. На самом деле я хотел взять известный список запросов, похожих на graphql, метапрограммно сгенерировать серверный код, который обслуживал бы только эти запросы, и сделать все это статически типизированным на каждом уровне. Мне давно хотелось поиграть с асинхронным Rust, и я взялся за работу. Некоторое время я занимался этим без перерыва.

У меня даже получилось заставить этот проект работать для многих типов запросов! Однако в какой-то момент я понял, что сам postgres на самом деле не настолько типобезопасен, как хотелось бы, поскольку он страдает от ошибки в миллиард долларов, позволяющей каждому значению быть потенциально нулевым. В репозитории Magmide я обсуждаю некоторые возможности Magmide, включая мутлиперсистентную метапрограммную базу данных, которой я намерен заняться после того, как Magmide заработает.

ts-std: 04.07.2019-26.02.2020

GitHub - marketdial/ts-std

github.com

Предыдущий проект - thin-ql - был первым, которым я серьезно занимался на Typescript. Я понял, что мне часто не хватает в нём различных абстракций, таких как удобные утилитарные типы и монады Result. В процессе работы над этим проектом я собрал абстракции в эту библиотеку, добавляя в нее по пути то, что мне приходило в голову. В конце концов, я перенес это репозиторий в организацию моего работодателя, так как мы начали активно использовать его в рабочих проектах.

kreia: 27.09.2019-16.02.2020

GitHub - blainehansen/kreia: A flexible and easy to use parser library. Look into chaos, and see order.

github.com

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

Этот период времени на самом деле является лишь самым последним толчком в этом проекте, когда я отрефакторил его из нетипизированного javascript, на котором он был изначально создан. Эта версия даже определяет свой собственный язык, специфичный для домена, для определения языковых грамматик, и из этих грамматик компилятор создает подмостки для парсера typescript, которые проект может заполнить пользовательской логикой. Я добился достаточной работоспособности, чтобы использовать его в других проектах, хотя там есть много неровностей и сложных случаев. Я намерен вернуться к этим концепциям, как только Magmide заработает (и, вероятно, даже раньше, чтобы заставить Magmide работать!), поскольку синтаксический анализ - это такая хорошо определенная логическая проблема, которая может значительно выиграть от проверки.

coq-playground: 22.01.2020-05.04.2020

GitHub - blainehansen/coq-playground

github.com

Примерно в это время я заинтересовался настоящим изучением Coq и начал читать Software foundations. Но на тот момент я ужасно боялся этого языка и не верил, что смогу использовать его для достижения чего-то. Я решил многие упражнения и был очарован этим инструментом, но был слишком напуган. Стоит ли уделять ему больше времени?

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

project-f: 10.03.2020-27.07.2020

GitHub - blainehansen/project-f

github.com

Как я уже упоминал ранее, меня крайне раздражало общее отсутствие типобезопасности в Vue. Мне нужен был глубоко типизированный фреймворк. Я считал, что Angular был слишком тяжелым и многословным (в чем я по-прежнему уверен), а шаблоны в стиле JSX были несуразными и поощряли недисциплинированное кодирование (во что я уже не очень верю). Мне также нравился язык шаблонов Pug и языки, чувствительные к пробельным символам, в целом (и до сих пор нравится). Так же импонировали многие концепции API Vue: однофайловые компоненты, простые обработчики событий компонентов, двусторонняя синхронизация компонентов, система слотов.

Учитывая все эти особенности, я решил создать собственный фреймворк для фронтенда (знаю, знаю), который с самого начала был бы типобезопасен сверху донизу, немагическую мелкозернистую реактивность и метапрограммные преобразования для обеспечения эргономичных API. У меня не было хороших идей для названия, так что я просто назвал его project-f от "project frontend".

Я снова добился того, что все в принципе работает! К тому времени, когда я закончил, можно было определить компонент в одном .iron файле и скомпилировать его в безопасный typescript. Однако я понял, что будет очень трудно заставить кого-либо использовать подобный фреймворк, если он не будет хорошо работать с существующими инструментами, такими как typescript-lsp и webpack. Поэтому я начал работать над решением и этой проблемы.

macro-ts: 09.07.2020-20.08.2020

GitHub - blainehansen/macro-ts: An ergonomic typescript compiler that enables typesafe syntactic macros.

github.com

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

Целью этого проекта было сделать макросы более естественными, чтобы предметно-ориентированный языки thin-ql и project-f, могли красиво интегрироваться с остальной частью окружающего их проекта. Я собирался начать использовать эту обертку компилятора для создания типобезопасного пакета приложений, но снова понял, что нет никакого смысла возиться с таким большим и неинтересным проектом, как Typescript. Проблема заключалась в Typescript и его отсутствии заботы о типобезопасности метапрограммирования, так что не было смысла продолжать решать эту проблему ради столь незначительного улучшения.

monads: 24.08.2020-27.08.2020

GitHub - blainehansen/monads

github.com

Это тот же код монад, который был написан в ts-std, но с немного улучшенным API (не было смысла менять оригинальный API, так как он довольно активно использовался у моего работодателя) с некоторыми макросами macro-ts, включенными в него.

validate: 27.08.2020-01.10.2020

GitHub - blainehansen/validate

github.com

В основном то же самое, что и monads, только я немного улучшил api и добавил несколько макросов. Также существенно доработал API для поддержки более сложных идей, таких как типы пересечения.

journalism-cooperative: 13.10.2020-03.11.2020

GitHub - blainehansen/journalism-cooperative

github.com

Долгое время я интересовался эффективным альтруизмом и логически обоснованными политическими реформами, такими как квадратичное голосование. В конце концов, я достаточно разочаровался в своих псевдосекретных и плохо продуманных технологических идеях, чтобы попытаться придумать себе другое полезное занятие. Я думал и писал об идеях других реформ, и одна из них была связана с постоянным голосованием и тем, как его можно использовать, чтобы сделать кооперативы гораздо более эффективными и конкурентоспособными.

Прочитав о том, как различные компании начинают создавать новые местные новостные компании, используя рассылки по электронной почте, я подумал, что эта модель может хорошо подойти для кооператива. Читайте об этом в этой статье в блоге. Сначала я подумал, что могу попытаться создать организацию сам и проделал некоторую работу по созданию базового сервера проверки электронной почты на Rust. Но понял, что не гожусь для управления такой организацией.

traya: 11.12.2020-11.02.2021

GitHub - blainehansen/traya

github.com

В этом проекте мы можем увидеть первые намеки на то, что мне надоел неверифицированный код. Я медленно двигался к тому, что делаю сегодня. В этом репозитории я играл с формализацией на Coq основных идей парсинга, которые можно было бы применить к более продвинутой LR-версии kreia (бонусные очки тем, кто знает почему kreia и traya связаны).

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

hopeful-pathway: ~01.07.2020-24.05.2021

GitHub - blainehansen/hopeful-pathway: An open source book charting a hopeful pathway for humanity.

github.com

Дата начала здесь немного расплывчата, поскольку изначально я составил многие эссе и заметки в ныне удаленном репозитории :facepalm:

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

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

Magmide: с 21.08.2020

GitHub - magmide/magmide: A dependently-typed language intended to make provably correct code possible for working software engineers.

github.com

Можно заметить, что репозиторий Magmide существует уже довольно давно. Даже эта дата, вероятно, недостаточно ранняя, поскольку в том же самом, ныне удалённом репозитории, в котором хранились многие из первых эссе hopeful-pathway, также хранилась куча заметок для этого проекта.

После моего первого знакомства с Coq я постепенно прочитал тонну различных ресурсов: о логике Хоара и логике разделения, теории типов и исчислении конструкций, лежащей в основе Coq, различные книги о Coq (например Certified Programming with Dependent Types), различные плагины и системы, построенные поверх Coq (такие как metacoq), различные проекты формализации для языков на всех различных уровнях иерархии абстракции и другие системы доказательства (Liquid Haskell, F* и Lean).

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

Оглядываясь назад на всю проделанную работу, я крайне разочарован в себе за то, что так испугался. Почти все вышеперечисленные проекты были либо полностью закрытыми, либо просто недостаточно широко распространялись, чтобы получить обратную связь... До сегодняшнего дня! Я сделал все эти репозитории общедоступными и написал людям способным сказать что-то полезное о проектах, на которые действительно стоит обратить внимание. Мне надоело прятаться, и я намерен работать с теми, кто поможет ввести формальную верификацию в массы и использовать ее для улучшения инфраструктуры программного обеспечения. Мы не можем больше ждать!

Мой путь к Magmide