Programming Language Choices for High Integrity Systems

Question

What programming languages are a good choice for High Integrity Systems?

An example of a bad choice is Java as there is a considerable amount of code that is inaccessible to the programmer. I am looking for examples of strongly typed, block structured languages where the programmer is responsible for 100% of the code, and there is as little interference from things like a JVM as possible.

Compilers will obviously be an issue. Language must have a complete and unambiguous definition.

EDIT: High Integrity Systems is an umbrella term for Safety Critical Systems etc, Secure Systems, etc.

EDIT EDIT: I want examples of languages that are not influenced by platform, that will produce the same result regardless of compiler and that are fully defined.

Answer 1

The SPARK subset of Ada would be a very good starting point. SPARK inherits all good features of Ada (strong typing, easy to read, ...) with the added benefit of having no undefined features, meaning that all SPARK programs will do the exact same thing, no matter which Ada compiler has been used to compile it.

SPARK can be used with no runtime. Similarly for the Ada language (see pragma No_Runtime).

Of course with languages such as SPARK you are trading flexibility for safety (or security).

Answer 2

I think ADA is commonly used for this.

Answer 3

How high integrety are you looking for?

• Galois in Portland, Oregon have built a very successful business on high-integrity systems written in Haskell. I believe they emphasize data integrity and security. It is somewhat surprising to do this kind of work in such a complex language, with a very complex run-time system, but Haskell's type system provides very strong guarantees, and the language semantics provide much stronger reasoning principles than most languages. Also, you tend to write much less code per application, so it is easy to show correct.

• If you need even stronger guarantees, SPARK Ada (or just SPARK these days) is a relatively simple, traditional imperative language that comes with a full formal semantics and tools for full formal verification. You get stronger guarantees than you would with Haskell, but at a mugh higher price, both in capital and labor.