Программировать сложно.

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

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

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

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

Путь Ржавчины

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

Правая часть диаграммы выше показывает проблемы параллелизма и безопасности памяти, которые принципиально невозможно разрешить в безопасном подмножестве Rust.

Таким образом, просто используя Rust, они могли предотвратить примерно половину ошибок того периода. Более того, ошибки внешнего доступа являются одними из самых опасных, так как они часто вызывают раскрытие секретов, отказ в обслуживании и удаленное выполнение кода, уязвимости.

Кроме того, это показывает, что таких идей, как «нужно просто уметь писать C» и «просто оставить низкоуровневые вещи профессионалам», недостаточно. Ядро Linux написано лучшими из лучших, 5% лучших в отрасли, и тем не менее, каждый год, снова и снова, мы получаем CVE из-за одних и тех же старых добрых ошибок памяти.

Конечно, эти 50 ошибок - ничто по сравнению с миллионами и миллионами строк рабочего кода. Но опять же, проблемы жизни и смерти, помните? Когда мы говорим о критических системах, даже самая маленькая ошибка может привести к катастрофическим последствиям. Не говоря уже о том, что это 50 ошибок, которые были обнаружены. Но кто знает, сколько их еще осталось? Используя Rust, мы заранее знаем ответ.

Насколько быстр Rust?

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

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

Как и в C ++, вы платите только за то, что используете. Например, в Rust вы используете мьютекс только тогда, когда вам это абсолютно необходимо. Более того, компилятор Rust заставит вас использовать его, так что вы никогда не забудете его добавить.

И все это практически без затрат. Поскольку большинство проверок выполняется во время компиляции, скомпилированная сборка не будет сильно отличаться от того, что генерирует компилятор C или C ++.

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

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

Почему мы используем Rust

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

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

Итак, с помощью Rust мы устраняем один из самых сложных и непредсказуемых классов ошибок.

Роль тестов

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

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

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

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

Сила математики

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

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

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

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

Ральф Юнг и др. из проекта RustBelt уже опубликовали некоторые статьи , которые доказывают, что заявленные фундаментальные инварианты языка Rust действительно сохраняются в некоторых важных примитивах стандартной библиотеки.

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

Чтобы доказать правильность стандартной библиотеки, Ральф Юнг с коллегами разработали подход к небезопасности, используя логику разделения и собственное исчисление, которое они назвали λrust. Используя это исчисление, они пытаются доказать, что стандартные библиотечные примитивы и контейнеры работают так, как задумано, и что они не нарушают фундаментальные инварианты Rust. В качестве побочного продукта они даже обнаружили пару ошибок в примитивах синхронизации, таких как MutexGuard и Arc.

Но эта работа далека от завершения. Как автор указывает:

Мы доказали, что далеки от всего, что есть в libstd. Для этого потребуется гораздо больше людей, чем мы можем собрать. Вместо этого мы сосредоточились на примитивах libstd, которые казались наиболее интересными и, казалось, больше всего подчеркивали систему типов. В основном это связано с внутренней изменчивостью. Таким образом, мы проверили Cell, RefCell, Rc, Mutex, RwLock, Arc и еще несколько отдельных методов, перечисленных в сообщении блога на бумаге.

Мы надеемся, что когда-нибудь мы сможем обеспечить такой же уровень доказательств правильности кода, написанного в Parity Technologies.

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

Первоначально опубликовано на сайте paritytech.io 3 июля 2018 г.