What is the programming language seen in The Martian?

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
}

realism the-martian

Best Answer

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.

Pictures about "What is the programming language seen in The Martian?"

What is the programming language seen in The Martian? - Woman Coding on Computer

What is the programming language seen in The Martian? - Close Up Photo of Programming of Codes

What is the programming language seen in The Martian? - High angle of pensive African American female freelancer in glasses and casual clothes focusing on screen and interacting with netbook while sitting at table with glass of yummy drink on cafe terrace in sunny day

What code is used in The Martian?

After putting signs for the 16 digits and numbers in a circle around Pathfinder, Watney combines the hexadecimal system with an ASCII table in both the book and movie. ASCII is a code that represents characters as numbers and is used to help display text onto computers among other devices.

What was the Mars rover programmed in?

It does appear that the testing scripts were written in Python. The underlying operating system is Wind River's VxWorks RTOS. The RTOS in question can be programmed in C, C++, Ada or Java. However, only C and C++ are standard to the OS, Ada and Java are supported by extensions.

What does NASA use for programming language?

HAL/S (High-order Assembly Language/Shuttle) is a real-time aerospace programming language compiler and cross-compiler for avionics applications used by NASA and associated agencies (JPL, etc.).

Does NASA use Python?

Internal sources within the critical project added that: \u201cPython allows us to tackle the complexity of programs like the WAS without getting bogged down in the language\u201d. Moreover, another indication NASA utilizes Python for their projects can be found from their mega 400 open-source projects that they publicly opened.

NASA Scientists Fact-Check “The Martian\

Sources: Stack Exchange - This article follows the attribution requirements of Stack Exchange and is licensed under CC BY-SA 3.0.

Images: Markus Spiske, ThisIsEngineering, luis gomes, Andrea Piacquadio