What is the programming language displayed on screenshot?
1
-
4Sweet jesus on a pancake, a non-monospaced font– Fabien Benoit-KochFeb 8, 2017 at 21:43
Add a comment
|
2 Answers
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.
answered Jan 17, 2016 at 13:46
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 :-) Mar 26, 2016 at 16:04