Оксид — Более Простая Формализованная Ржавчина

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

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

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

В отличие от Go, Rust-более сложный язык для изучения и правильного использования, но он действительно приносит некоторые новые вещи на стол. Цитата из газеты:

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

Как я уже сказал, ржавчина особенная. Они также указывают на проблему крутой кривой обучения:

«Несмотря на свой успех, Rust также приобрел некоторую репутацию своей сложности среди программистов. Нередко можно услышать, как люди обмениваются рассказами о борьбе с проверкой заимствований после того, как окунули пальцы ног в ржавчину. Естественно тогда задаться вопросом, является ли этот опыт неизбежным. Мы говорим, что нет! Хотя, вероятно, более мощной системе типов присуща некоторая сложность, мы считаем, что фундаментальная проблема, стоящая перед нами, более ясна, а именно, трудно изучать новую семантику.»

Как человек, который все еще учится использовать Rust, я понимаю, к чему они клонят, но я не рассматриваю это как «борьбу с проверкой заимствования», а скорее пытаюсь изучить новый способ мышления, который применяет проверка заимствования.

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

Оксид, который был описан в статье arxiv Николасом Мацакисом из Mozilla Research и Аароном Вайсом, Дэниелом Паттерсоном и Амал Ахмедом из Северо-Восточного университета, является попыткой найти сущность ржавчины. Идея заключается в том, что, найдя формальное выражение конкретной семантики Rust, можно было бы найти лучшие способы ее представления. Читая эту статью, вы получаете более глубокое понимание того, как Rust управляет ссылками и временем жизни. Я не уверен, что в конце концов оксид предпочтительнее ржавчины, и как только вы попадете в формальную семантику, это будет только для специалистов.

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

Дайте ржавчине попробовать, но не ожидайте, что это будет легкий переход.

Гарри Фэрхед-автор фундаментального C: Close to the Machine (I/O Press).