Что делают разработчики языка, чтобы решить или доказать, что определенная функция работает правильно?

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

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

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

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

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

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

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

• Или есть формальный способ на самом деле доказать (в математическом смысле слова), что ваша функция работает, а затем использовать это доказательство, чтобы уверенно получить правильную (или в основном правильную) функцию с самого начала?

(Я должен отметить, что у меня есть инженерное образование, а не компьютерные науки. Поэтому, если я упускаю что-то, что было бы очевидно для людей из CS, пожалуйста, не стесняйтесь указывать на это.)

У меня проблемы с поиском точной ссылки на данный момент, но некоторое время назад я посмотрел несколько видео Саймона Пейтона Джонса , который внес основной вклад в дизайн Haskell. Между прочим, он является отличным докладчиком по теории типов, языковому дизайну и тому подобному, и у него есть много бесплатных видео на YouTube.

У Haskell есть промежуточное представление, которое по сути является лямбда-исчислением, дополненным несколькими простыми вещами, с которыми легче работать. Лямбда-исчисление использовалось и доказывалось, так как компьютер был просто человеком, который вычислял вещи. Интересный момент, который Саймон Пейтон Джонс часто делает, состоит в том, что всякий раз, когда они делают что-то дикое и сумасшедшее с языком, он знает, что это принципиально правильно, когда в конечном итоге он возвращается к этому промежуточному языку.

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

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

Для языковой реализации это код, как и любой другой. Вы пишете юнит-тесты. Вы пишете интеграционные тесты. Вы делаете обзоры кода.

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

Практически , сравнительно немного языков используют доказательства для проверки их функциональности, и в итоге получают несколько вариантов, которые вы упоминаете.

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

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

Для руководства в этом вопросе дизайнер опирается на набор правил и принципов дизайна. Этот подход очень хорошо описан в « Проектировании и развитии C ++ » Бьярна Страуструпа , одной из редких книг, посвященных языковому дизайну. Что очень интересно, так это то, что языки редко разрабатываются в вакууме, и дизайнер также смотрит, как их языки реализовали аналогичные функции. Другим источником (онлайн и бесплатно) являются принципы дизайна для языка Java .

Если вы посмотрите на публичные слушания комитетов по стандартизации, то увидите, что это скорее пробная ошибка. Вот пример на модуле C ++ полностью новая концепция, которая будет представлена ​​в следующей версии языка. И здесь анализ составлен после некоторых языковых изменений , чтобы оценить его успех. И вот процесс сообщества Java для определения новых спецификаций Java, таких как новый API . Вы увидите, что эту работу выполняют несколько экспертов, которые творчески разрабатывают концептуальный документ и первое предложение. Затем эти предложения рассматриваются большим сообществом / комитетом, который может изменить предложение, чтобы обеспечить более высокую степень согласованности.

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

Каждая новая функция может взаимодействовать со всеми другими функциями. (Это влияет на язык, документы, компиляторы, сообщения об ошибках, IDE, библиотеки и т. Д.) Объединяются ли функции, чтобы открыть лазейку? Чтобы создать неприятные крайние случаи?

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

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

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

Другими словами, удобство использования так же важно для языкового дизайна, как и для других видов дизайна. Это влечет за собой (1) дизайн для удобства использования (например, зная вашу аудиторию), и (2) тестирование удобства использования.

Пример статьи на эту тему: « Программисты - это люди, и язык программирования, и разработчики API могут многому научиться в области проектирования с учетом человеческого фактора».

Пример вопроса SE на эту тему: Синтаксис любого языка программирования проверен на удобство использования?

В качестве примера теста удобства использования рассматривалось расширение функции итерации списка (я не помню, на каком языке), чтобы принимать несколько списков. Люди ожидали, что он будет перебирать списки параллельно или через перекрестный продукт? Разработчики языка были удивлены результатами теста юзабилити.

Такие языки, как Smalltalk, Python и Dart, были разработаны с упором на удобство использования. Ясно, что Хаскелла не было.