Перевод статьи https://cexplorer.io/article/why-did-iog-choose-haskell-to-build-cardano
Команда IOG тщательно определялась с тем, какой язык программирования и инструменты использовать для разработки Cardano. В конце концов, они выбрали Haskell. Команда должна иметь возможность формально подтвердить, что все, написанное в белой книге, будет должным образом соответствовать написанному исходному коду. Приглашаем почитать о том, как команда преобразует математические доказательства из белой книги в исходный код Haskell.
TLDR:
- До Cardano ни один проект из топ-10 не использовал формальные методы.
- Белая книга является основой для формальной спецификации. Это основа для исходного кода, написанного на Haskell.
- Формальная спецификация и исходный код Haskell имеют очень похожие обозначения.
От белой книги к исходному коду
У многих команд в блокчейн индустрии есть менталитет стартапа “двигайся быстро и ломай вещи”. Этим менталитетом движут молодость, жадность и страсть. Исходный код многих протоколов часто пишется в спешке и без предварительного исследования. В некоторых случаях можно говорить о безответственном подходе команд к пользователям. Противоположность - это медленный, методичный и академически ориентированный подход, мотивированный желанием закрепить инновации в нашем пространстве. В то время, когда команда начала разрабатывать Cardano, ни одна из десяти крупнейших криптовалют по рыночной капитализации не была основана на проверенном протоколе и не была реализована на основе формальной спецификации. Команда IOG решила использовать формальные методы для разработки Cardano.
Команда IOG определяет и математически доказывает правильность поведения протокола и других компонентов в белых книгах. Затем они используются для создания формальной спецификации. Формальная спецификация - это точное математическое описание поведения и свойств системы.
В белых книгах математические обозначения используются для выражения абстрактных понятий и математических доказательств. Они точны, но неспециалистам могут быть трудны для понимания. Формальная спецификация используется для выражения поведения и свойств программной системы точным математическим способом. Она менее абстрактна, чем математические обозначения, но более точна, чем исходный код. Другими словами, программист может не понимать математические обозначения, используемые в белых книгах, но способен понять формальную спецификацию.
После создания формальной спецификации следующим шагом является реализация исходного кода на языке программирования Haskell. Ожидается, что реализация соответствует спецификациям и свойствам, описанным в формальной спецификации. Реализация должна быть выполнена таким образом, чтобы можно было математически доказать, что реализация соответствует требованиям и свойствам, описанным в формальной спецификации. Другими словами, исходный код может быть формально проверен на основе спецификации.
Исходный код Haskell используется для выражения реализации Cardano. Это наиболее конкретная форма ожидаемого поведения. Это форма, в которой выполняется система. Исходный код Haskell менее точен, чем обозначения формальных спецификаций, но разработчикам Haskell его легче понять.
Несмотря на то, что существует взаимосвязь между математическими обозначениями, формальной спецификацией и исходным кодом Haskell, переключаться между ними не всегда легко. Уровень абстракции и выразительности каждого из них различен, поскольку используются разные обозначения. Цель состоит в том, чтобы максимально упростить передачу информации между различными обозначениями.
Ученые и математики не обязательно должны быть программистами на Haskell. Их работа состоит в том, чтобы написать белую книгу. Программистам на Haskell не обязательно быть лучшими математиками. Формальная спецификация является своего рода посредником между двумя группами. Должен быть кто-то, кто способен создать формальную спецификацию на основе белой книги. Однако можно использовать инструменты, которые могут автоматически переводить между математическими обозначениями, обозначениями формальной спецификации и исходным кодом, такие как языки программирования с зависимой типизацией, такие как Coq или Agda.
Cog и Agda являются формальными инструментами проверки, которые могут быть использованы в контексте функциональных языков программирования, таких как Haskell. Они оба являются помощниками по проверке, которые представляют собой компьютерные программы, помогающие пользователям писать формальные математические доказательства.
И Cog, и Agda основаны на идее использования формальных методов для повышения надежности и корректности программных систем. В то время как Cog более специфичен для параллельных алгоритмов, Agda является более общим и может использоваться для любого вида функционального программирования. Оба они являются мощными инструментами для обеспечения корректности программных систем и могут использоваться вместе для обеспечения комплексного решения по проверке.
Почему Haskell
Haskell - это функциональный язык программирования, который хорошо подходит для использования формальных методов при разработке программного обеспечения.
Одним из главных преимуществ Haskell является его сильная система типов. В Haskell есть система статических типов, которая означает, что типы проверяются во время компиляции, обеспечивая высокий уровень безопасности и предотвращая многие типы ошибок еще до запуска программы. Кроме того, Haskell поддерживает вывод типов, что означает, что программисту не нужно явно указывать типы переменных и функций, что делает код более кратким и читаемым.
В Haskell переменные по умолчанию неизменяемы, что означает, что как только переменной присваивается значение, оно не может быть изменено. Это облегчает рассуждения о поведении программы и может упростить параллельное программирование. Неизменяемость также помогает предотвратить ошибки, вызванные неожиданными изменениями переменных, а также делает код более тестируемым.
Haskell также уделяет большое внимание функциональному программированию, что поощряет декларативный и выразительный стиль программирования. В функциональном программировании основное внимание уделяется описанию того, что должна делать программа, а не того, как она должна это делать. Это делает код более читаемым и поддерживаемым, а также может упростить отладку и тестирование.
Сильная система типов Haskell и математический стиль программирования делают его естественной для формальных методов. Система типов в Haskell очень выразительна, обеспечивая высокий уровень статической проверки кода. Это означает, что многие распространенные ошибки программирования могут быть обнаружены во время компиляции, а не во время выполнения. Кроме того, парадигма функционального программирования поощряет математический стиль мышления, который помогает сделать код более предсказуемым и о нем легче рассуждать. Это может быть особенно полезно для сложных и больших кодовых баз Cardano.
Сборка мусора в Haskell и строгая оценка гарантируют, что программа защищена от ошибок во время выполнения, таких как разыменование нулевого указателя, переполнение буфера и гонка данных. Это делает его более подходящим для систем, критически важных для безопасности.
Модель параллелизма Haskell основана на облегченных потоках, а передача сообщений упрощает написание кода, который может использовать преимущества нескольких ядер и процессоров. Это важно для проекта Cardano, который представляет собой блокчейн платформу, которой необходимо обрабатывать большое количество транзакций одновременно.
Высокоуровневые абстракции Haskell, такие как монады, облегчают написание модульного, составного и многоразового кода. Это может помочь уменьшить сложность кодовой базы и облегчить рассуждения о свойствах кода и их доказательство.
Функция факториала
Давайте рассмотрим простой пример того, как математическое обозначение может быть преобразовано в исходный код.
Полное математическое доказательство функции факториала выглядело бы примерно так:
Вот как выглядит формальная спецификация в Agda для функции факториала:
Вот так выглядит обозначение Coq функции факториала:
Посмотрите, как исходный код функции факториала Haskell напоминает обозначения Agda и Coq:
Для сравнения посмотрите, как выглядит реализация функции факториала в традиционном языке C++:
Программист должен понимать формальную спецификацию, чтобы иметь возможность написать соответствующий исходный код на Haskell. Конечно, программист также может написать функцию факториала на C++, но обратите внимание, что обозначения менее похожи на формальную спецификацию. Код в обоих случаях делает именно то, что указано в спецификации, и это самое важное из всего.
Однако для программиста более естественно сравнивать обозначение Haskell и формальные спецификации, чем если бы ему пришлось делать то же самое с C++ (или другим подобным языком). Разница была бы более заметна для более сложных функций.
Вывод
У команды IOG было много причин выбрать Haskell. Важен не только сам язык, но и его пригодность для решения конкретной задачи, количество доступных инструментов и количество качественных разработчиков. Обычному программисту не очень часто приходится иметь опыт работы с формальными методами. В случае программистов на Haskell частота выше. Более того, редко можно найти опытных разработчиков Haskell без детальных знаний в области компьютерных наук.
В контексте необходимости использования формальных методов для разработки Cardano Haskell был одним из естественных вариантов. Cardano создается как критически важный проект, и Haskell имеет в своей ДНК функции, которые помогают достичь этой цели.
// От переводчика: для получения дополнительных переведенных на русский язык статей о Cardano посетите русскоязычный раздел на форуме Cardano. Видеоролики о Cardano на русском можно найти на YouTube канале нашего замечательного амбасадора Тимура Сахабутдинова, а также на канале Чарльз Хоскинсон на русском. Хотите поговорить или задать вопрос о Cardano по-русски? Приглашаем вас в наше уютное сообщество в Telegram. Оставайтесь на связи, все только начинается!