Since the release of the science fiction film The Martian in 2015, movie fans have been speculating in internet forums about the source code that is displayed in computer screens in some scenes of the movie. Some fans have jokingly guessed “alien technology”, others claimed to be “gibberish”, and the most informed have noticed similarities with programming languages such as as Lisp, Prolog, and, even, Pascal.
Closest to the truth, the Internet Movie Database (IMDb) explains:
Whenever Mark boots up a computer (ie. when finding the MAV) a sequence of source code is seen appearing on a screen. The code is written in PVS (Prototype Verification System), an experimental macro language which NASA actually uses and it's very plausible to appear on a future spacecraft. This particular chunk of code is from the already existing NASA PVS Library, and actually you can find that very piece of code as open source if you type a part of it into Google.
Indeed, the source code seen in the movie The Martian is written in PVS, a verification system developed by SRI International. It is also true that this particular code is part of the NASA PVS Library, a collection of formal theories developed and maintained by the Formal Methods Group of the Safety-Critical Avionics Systems Branch at NASA Langley Research Center. However, PVS is neither a programming language, nor a “macro language”. PVS is a proof assistant. It consists of a specification language, i.e., a formal notation for defining mathematical objects and their properties, and an interactive theorem prover for verifying these properties using deductive rules. Both PVS specifications and proofs are displayed in the movie.
Code from the NASA PVS Library appears three times in the
movie. In every instance, the code is unrelated to the movie's implied
functionality. At 58 minutes, the following snippet of code from the file
power/exponentiation_aux.prf is shown
in a computer screen in the Hermes spacecraft.
("" (induct "n") (("1" (expand "expt") (("1" (propax) nil nil)) nil) ("2" (skosimp*) (("2" (expand "expt" 1) (("2" (inst - "px!1") (("2" (lemma "both_sides_times_pos_le1" ("pz" "px!1" "x" "1" "y" "expt(1+px!1,j!1)")) (("2" (rewrite "expt_gt1_bound1" -1) (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)
It is implied in the movie that this text encodes video data. In
reality, this text is the PVS internal representation of a proof of the
the mathematical statement
, where is a natural
number and is a positive
Internally, PVS uses
s-expressions to represent proofs. PVS is implemented in Lisp and s-expressions are often used in Lisp
programs to represent data.
s-expressions are constructed by PVS from proof commands entered by the
user such as
(expand "expt"), etc.
This s-expressions reflects the fact that the proof, which was written by Prof. David Lester (U. of Manchester, UK), proceeds by
induction on .
mpoly : VAR MultiPolynomial mdeg : VAR DegreeMono mcoeff : VAR Coeff nvars,terms : VAR posnat rel : VAR RealOrder Avars,Bvars : VAR Vars boundedpts, intendpts : VAR IntervalEndpoints MPoly : TYPE = [# mpoly : MultiPolynomial, mdeg : DegreeMono, terms : posnat, mcoeff : Coeff #] mk_mpoly(mpoly,mdeg,terms,mcoeff) : MACRO MPoly = (# mpoly := mpoly, mdeg := mdeg, terms := terms, mcoeff := mcoeff #)
The movie implies that this code is somehow related to the shutdown and startup scripts of the Mars Habitat (Hab) and the Mars Ascending Vehicle (MAV), respectively. Indeed, this code is a PVS specification of a data structure for representing multivariate polynomials. The code, which was written by Anthony Narkawicz (NASA) and César Muñoz (NASA), is part of a PVS formalization of a method for approximating the minimum and maximum values of a multivariate polynomial using Bernstein polynomial basis.
What about the claim by the Internet Movie Database (IMDb) that PVS code will appear in future spacecraft? Unlikely. As explained here, PVS is not a programming language but a proof assistant. Unless astronauts would like to kill the tedium in a long interstellar voyage by proving theorems, PVS won't be installed in future spacecraft computers. However, it is possible that computer programs, whose safety-critical algorithms have been formally verified in PVS, would appear in future aerospace systems. That is the case of separation assurance systems for air traffic management such as ACCoRD and detect and avoid systems for unmanned aircraft systems such as DAIDALUS.The tag identifies links that are outside the NASA domain