NASA PVS Library Featured in the Movie “The Martian”

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 real number. 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. These s-expressions are constructed by PVS from proof commands entered by the user such as (induct "n"), (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 .

The second and third appearances of the NASA PVS Library occur at times 1h:39m:03s and 1h48m53s, respectively, when the following code from Bernstein/MPoly.pvs is displayed in a computer screen.

  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