Какой язык программирования используется в The Martian?

Похоже, это PVS , вариант языка Лиспа, также связанный с Прологом. См. также страницу спецификации PVS . Этот конкретный фрагмент кода взят из библиотеки NASA PVS , и вы можете найти его в файлах Bernstein/MPoly.pvs.

Фрагмент, который вы видите на изображении, действительно является частью PVS, написанной Энтони Наркавичем и Сезаром Мунозом, оба из НАСА, Лэнгли, Вирджиния, США. Однако это не язык программирования, а интерактивное средство доказательства теорем.

Язык состоит из двух частей: способ изложения теорем (файлы .pvs) и способ изложения доказательств (файлы .prf). Пример последнего из одного из моих пруфов можно увидеть в кадре из фильма по ссылке здесь .

Конечно, настоящий вопрос заключается в том, почему персонажу Мэтта Деймона нужно доказательство свойств экспоненциальной функции, чтобы избежать затруднительного положения. Возможно, это станет очевидным, когда я увижу фильм!