Programming Language Choices for High Integrity Systems

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开发者_JAVA百科 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.

---

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).

---

I think ADA is commonly used for this.

---

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.

---

You might want to think in terms of Eiffel, where the stronger enforcement of pre- and post-conditions make high-integrity systems easier.

---

This is a contradiction in terms. Strongly typed, block-structured languages are almost always compiled by a compiler, producing machine code that the programmer is not responsible for. If you want to be 100% responsible for the code, you need to use assembly language.

---

I don't fully understand what it a "high-integrity system". Assuming that you mean "a system that leave less place for bugs", I suggest you take a look at ML, and it's OOP derivative, O'CaML. ML was designed to minimize type errors. There are no casting errors or null pointers in ML - You simply can't code them. It also lacks dynamic features - Which makes it less cool but safer.

Having said that, ML is far from being a hackers' delight; It's a somewhat cumbersome language. But if you prefer to work an hour more and get one exception less, it's a relevant choice.

---

You may look for what you want, but you won't get it.

Your requirements are not compatible with each other. They basically totally rule out any sort of library. You can say you can use C / C++ - but WITHOUT ANY INCLUDE FILES AND STANDARD LIBRARIES (for which the programmer would obviously not be responsible).

This leaves you pretty much in dry land - the requirement is unrealistic. Even with a large team, one would not want to reprogram most libraries.

Java is pretty good actually if you have the proper programming methods in place - and interesting enough your requirement (high integrity system) is much more an issue of programming methodology (unit tests, tons of internal tests, multiple instances in parallel comparing results - like space shuttle control computers - in case one malfunctions) than something the language decides.