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

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

Немного истории и социологии

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

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

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

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

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

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

Таким образом, очевидно, что нам нужны более эффективные способы создания надежного программного обеспечения.

О математиках, реальности и человеческой ошибке

В этот момент вы, вероятно, думаете: «Хорошо, Statebox - это просто еще один язык программирования, обещающий стать следующим большим достижением». Почему-то вы правы, но позвольте мне сказать вам, в чем то, что мы делаем, отличается. Я математик, и большую часть своей жизни я посвятил изучению полностью рациональных, неизменных, совершенных систем. Вывод, который я получил отсюда, заключается в том, что применение этой точки зрения к реальному миру вызывает только проблемы. Количество непредвиденных / непредсказуемых / неучтенных материалов, которые всплывают, когда вы пытаетесь использовать математику Моделирование реальных явлений таково, что чаще всего вы в конечном итоге очень разочаровываетесь - как в своей модели, которая на самом деле не работает, так и в реальности, которую иногда бывает чрезвычайно трудно приручить. Это не то, что можно исправить с помощью математики, и это связано с внутренней сложностью самой реальности.

К сожалению, многие теоретики привыкли рассуждать в рамках своих совершенных моделей и не полностью осознают, как вещи сделают все, что в их силах, чтобы разрушить их мечты, когда их модели будут реализованы. Что касается безопасных, надежных языков программирования, я слышал, как многие люди и компании утверждали, что у них есть что-то «совершенно последовательное, проверенное, математически великолепное и это JUSTWORKS ™». Это очень хорошо и, безусловно, необходимое условие для разработки языков программирования будущего, но этого недостаточно. Что не учитывается в этом рассуждении, так это то, что в большинстве случаев ошибка связана с человеком.

Например, подумайте о компиляторе C. Это, пожалуй, одно из самых великолепных произведений искусства, о которых вы только можете подумать. Проверено более тридцати лет, невероятно эффективно, практически без ошибок. Тем не менее, создать неправильный код на C очень легко, и это потому, что C трудно использовать, когда дело доходит до превращения сложных идей в код. Короче говоря, очень легко написать код, который не делает то, что вы думаете.

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

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

Простое предложение

Типовая разработка с Idris Эдвина Брэди - это произведение искусства. Это не просто книга о функциональном программировании - более того, обучающая вас Идриса, который является довольно сложным и, казалось бы, неизвестным функциональным языком, - это книга, объясняющая, почему программирование с использованием типов - это здорово.

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

В Statebox, когда мы увидели такой способ написания программного обеспечения, мы сразу влюбились в него, но решили амбициозно поднять ставки другим предложением:

Что, если мы сможем получить полное и последовательное разделение между топологией программного обеспечения и смыслом?

Разделение

Концепция разделения вещей таким образом, чтобы они были двумя сторонами одной медали - очень важная концепция в математике и теоретической информатике. Разделения как таковые есть повсюду: синтаксис и семантика в логике, операционная и денотационная семантика в языках программирования и так далее. Идея разделения заключается в том, что если, с одной стороны, вы хотите описать некую структуру с одной точки зрения (т.е. как формальную систему), с другой стороны, вы хотите описать ту же структуру с другой точки зрения (т.е. какое значение имеет эта структура). Затем вы хотите доказать, что эти описания четко связаны друг с другом предсказуемым образом. Если это у вас есть, то вы можете плавно переключаться с одной точки зрения на другую последовательным образом, позволяя для раздельного мышления.

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

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

Чтобы дать вам простой пример этого, на рисунке ниже представлена ​​квантовая телепортация (Я не шучу, это не шутка).

Благодаря формальным связям между этим графическим формализмом и определенным классом категорий (в данном случае компактными замкнутыми категориями) это не просто картинка, а теорема. Я могу буквально перевести этот рисунок в линейную алгебру с помощью компьютерной программы и получить классическое математическое описание телепортации.

В следующих сообщениях я немного подробнее расскажу, как работает Statebox, но на данный момент я хочу, чтобы вы получили следующее: представьте себе язык программирования, который является в значительной степени формальным, где можно писать правильно, проверено -по умолчанию. А теперь представьте, что все, что вы делаете в Statebox, имеет графическое изображение. Вы можете буквально нарисовать форму своего программного обеспечения и впоследствии наполнить ее смыслом последовательным образом. Вы можете постоянно визуально отлаживать то, что делаете. Вы действительно можете создать продукт вместе со своими клиентами, которые, возможно, впервые в своей жизни могут осмысленно понять разработку программного обеспечения и помочь вам, часто просто указывая, что «эта часть чертежа на самом деле не кажется, уловил то, что я имел в виду ».

В Statebox мы не только пытаемся повысить надежность и эффективность с помощью математических расчетов, мы также пытаемся уменьшить количество человеческих ошибок и максимально приблизиться к безупречной реализации кода. К чему это сводится использует «очевидные», «простые» вещи, то есть дополняет формально структурированную среду пространственной интуицией.

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