Пересматривал с женой "Марсианина". На глаза попался код на экране, который не выглядел стандартной смесью HTML и старофранцузского.
С первого взгляда подумал о Lisp, потом - о каком-то диалекте Prolog-а.
Я вышел в интернет с таким вопросом и нашёл статью на сайте NASA с разбором этого кода!
Оказывается это описание теоремы на макросах Common Lisp для системы автоматического доказательства теорем PVS (Prototype Verification System). Само описание входит в состав библиотеки NASAlib от исследовательской группы формальных методов исследовательского центр Лэнгли.
Этот код по-прежнему не подходит по смыслу к сцене фильма (в которой происходит отправка телеметрии), но всё же любопытнее обычной овсянки :)
- статья от NASA https://shemesh.larc.nasa.gov/fm/pvs/TheMartian/
- PVS пруфер https://pvs.csl.sri.com/description.html и его сорцы https://github.com/SRI-CSL/PVS
- NASALib https://github.com/nasa/pvslib
