That's technically true, but if NASA's API accepted arguments in Meters instead of int32_t (or whatever the equivalent was in the language they used), then it would've been instantly obvious that the controller code that Lockheed Martin wrote was using the wrong datatype.

Do we know how the code was called, was it linked in or was it via IPC (the latter seems most likely to me, and then the question is does the IPC framework support a rich type system)?