What is the programming language seen in The Martian?

Question

In the "systems shutdown" scene in The Martian, they show some code. Is that a real programming language (best guess Haskell) or just some hacking-movie-fake-code-with-random-math thing?

Sample:

mpoly        : VAR MultiPolynomial
msdeg        : VAR DegreeMonomcoeff      : VAR Coeff
mvars,terms     : VAR posnatrol        : VAR RealOrder
Avars,Bvars   : VAR Varboundedpts,
Intendpts   : VAR IntervalEndpoints

MPoly : TYPE = {#
  mpoly  : MultyPolynomial
  mdeg  : Degree Means, terms : posnat
  mcoeff  =L Coeff
}

Answer 1

According to this blog, it's not a programming language, but instructions for a proof assistant:

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.

The part you identified is discussed as well:

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.