What is the programming language displayed on screenshot?
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!