От переводчика:
Предлагаю вашему вниманию перевод двух постов из блога John Regehr. Я решил объединить их в одной публикации потому, что, во первых, они имеют небольшой объём, и, во-вторых, второй пост является продолжением первого, и является ответом на комментарий к первому посту на Hacker News.

Ссылка на первый пост
Ссылка на второй пост

Часть 1. Неопределённое поведение != Небезопасное программирование

Неопределённое поведение (UB) в C и C++ представляет собой опасность для разработчиков, особенно если код работает с недоверенными данными. Менее известно, что неопределённое поведение существует в промежуточном представлении (IR) большинства оптимизирующих AOT компиляторов. Например, LLVM IR имеет значение undef и «отравленные» значения в дополнение к взрывоопасному UB языка С. Когда люди начинают беспокоиться об этом, типичная реакция такова: “Что? LLVM IR так же плох, как и C!” Эта статья объясняет, почему считать так неверно.

Неопределённое поведение — это результат проектного решения: отказ от систематизированного обнаружения программных ошибок на определённом уровне системы. Ответственность за то, чтобы таких ошибок не было, возлагается на более высокий уровень абстракции. Например, очевидно, что безопасный язык может быть скомпилирован в машинный код, но также очевидно, что небезопасность машинного кода возлагает все бескомпромиссные высокоуровневые гарантии на реализацию языка. Swift и Rust компилируются в LLVM IR; некоторые их гарантии безопасности осуществляются динамическими проверками в генерированном коде, другие производятся с помощью проверки типов и не представлены на уровне LLVM IR. Другими словами, UB на уровне LLVM не обнаруживается и является проблемой кода из безопасного подмножества языков Swift и Rust. Даже C может быть использован безопасно, если какой-либо инструмент в среде разработки убедится в отсутствии UB. Проект L4.verified делает именно это.

Суть неопределённого поведения заключается в том, что оно позволяет избежать связи между операциями проверки на ошибку и небезопасными операциями. Проверки, будучи несвязанными с небезопасными операциями, могут быть удалены оптимизатором, или, как вариант, вынесены из цикла. Оставшиеся небезопасные операции могут быть, при хорошо спроектированном IR, отображены на операции процессора с минимальными накладными расходами, или вообще без таковых. Для примера рассмотрим следующий код на Swift:

func add(a : Int, b : Int)->Int {
  return (a & 0xffff) + (b & 0xffff);
}

Несмотря на то, что реализация Swift должна захватывать исключение при переполнении целого, компилятор видит, что переполнение невозможно и генерирует такой LLVM IR:

define i64 @add(i64 %a, i64 %b) {
  %0 = and i64 %a, 65535
  %1 = and i64 %b, 65535
  %2 = add nuw nsw i64 %0, %1
  ret i64 %2
}

Не только операция сложения с проверкой переполнения была заменена на операцию сложения без проверки, но также инструкция сложения была помечена атрибутами nsw и nuw, которые обозначают, что и знаковое, и беззнаковое переполнение не определено. Сами по себе эти атрибуты не приносят выгоды, но могут вызвать дополнительные оптимизации, если функция будет заинлайнена. Когда набор тестов Swift компилируется в LLVM, только одна инструкция сложения из восьми имеет атрибут, указывающий, что переполнение целого не определено.

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

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

Часть 2. Всегда ли выразительный язык программирования имеет неопределённое поведение?

На Hacker News кто-то так прокомментировал мой предыдущий пост:

ЕМНИП, теорема о неполноте Гёделя подразумевает, что любой язык имеет по крайней мере в некоторой степени неопределённое поведение.

Давайте посмотрим на это утверждение, помня о том, что неполнота и неразрешимость — довольно сложные вещи. Много лет назад я с удовольствием прочитал теорему Гёделя: "неполнота приводит к злоупотреблениям" (мне несомненно нужно её перечитать).

Во-первых, существуют языки программирования без UB, например, такой язык, что любая программа на нём печатает «7». Что бы ни означало UB (мы пока не дали формального определения), ясно, что язык, который всегда печатает «7» его не имеет.

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

Но на самом деле, комментатор с HN имел в виду теорему Райса: «любое нетривиальное свойство языка, распознаваемого машиной Тьюрига, неразрешимо.» Вследствие этого, если f() — некоторое произвольное вычисление, мы не можем в общем случае решить, вызывает ли программа неопределённое поведение:

main() {
  f();
  return 1 / 0; // UB!
}

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

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