What is the programming language displayed on screenshot?

strange programming language

  • 4
    Sweet jesus on a pancake, a non-monospaced font Commented Feb 8, 2017 at 21:43

2 Answers 2


It seems like this is PVS, a Lisp variant language, also related to Prolog. See also the PVS specification page. This particular piece of code is from the NASA PVS library, and you can find it in Bernstein/MPoly.pvs.


The fragment you see in the image is indeed a piece of PVS, written by Anthony Narkawicz and Cesar Munoz, both of NASA Langley, Va, USA. However, it is not a programming language, but instead an interactive theorem prover.

There are two parts to the language: a way to state theorems (.pvs files) and a way to state proofs (.prf files). An example of the latter from one of my proofs can be seen in a still from the film using the link here.

Of course the real question is why Matt Damon's character needs a proof about properties of the exponential function to escape his predicament. Perhaps that will become apparent when I get to see the film!

  • +1 for a good answer, and for being based down the road from me :-) Commented Mar 26, 2016 at 16:04

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service and acknowledge you have read our privacy policy.