24

What is the programming language displayed on screenshot?

strange programming language

  • 4
    Sweet jesus on a pancake, a non-monospaced font – Fabien Benoit-Koch Feb 8 '17 at 21:43
30

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.

| improve this answer | |
13

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!

| improve this answer | |
  • +1 for a good answer, and for being based down the road from me :-) – maguirenumber6 Mar 26 '16 at 16:04

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy