Choice of programming language for systems with a high degree of integrity

Question

Which programming languages ​​are a good choice for systems with a high degree of integrity?

An example of poor choice is Java, since there is a significant amount of code that is not available to the programmer. I am looking for examples of strongly typed, structured blocks, where the programmer is responsible for 100% of the code, and as little interference as possible from things like the JVM.

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

EDIT: Systems with a high degree of integrity are an umbrella term for mission-critical security systems, etc., Protected systems, etc.

EDIT EDIT: I want examples of languages ​​that are not affected by the platform, which will give the same result regardless of the compiler and are fully defined.

Answer 1

A subset of SPARK Ada would be a very good starting point. SPARK inherits all the good Ada functions (strong typing, easy to read, ...) with the added benefit of not having undefined functions, which means that all SPARK programs will do the same, no matter which Ada compiler was used to compile it.

SPARK can be used without runtime. Similarly for the Ada language (see Pragma No_Runtime).

Of course, with languages ​​like SPARK, you trade flexibility for security (or security).

Answer 2

I think ADA is commonly used for this.

Answer 3

How can you find high intelligence?

• Galois in Portland, Oregon, has created a very successful business with high integrity systems written in Haskell . I believe that they emphasize data integrity and security. It's amazing to do this kind of work in such a complex language, with a very complex runtime system, but a system like Haskell provides very strong guarantees, and the semantics of the language provide much stronger reasoning principles than most languages. In addition, you tend to write much less code for each application, so it is easy to show correctly.

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

Answer 4

Perhaps you should think in terms of Eiffel , where more stringent compliance with preconditions and post-conditions makes high system integrity easier.

Answer 5

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

Answer 6

I do not quite understand that this is a "system with a high degree of integrity." Assuming you mean “a system that leaves less room for errors,” I suggest you take a look at ML , and this is a derivative of OOP, O'CaML . ML was designed to minimize type errors. There are no cast errors or null pointers in ML. You simply cannot encode them. It also has no dynamic features - which makes it less cool, but safer.

Having said that, ML is far from enjoying hackers; This is a somewhat cumbersome language. But if you prefer to work an hour more and eliminate one exception, this is an important choice.

Answer 7

You can search for what you want, but you will not receive it.

Your requirements are incompatible with each other. They basically completely exclude any library. You can say that you can use C / C ++, but WITHOUT ANYTHING, INCLUDE FILES AND STANDARD LIBRARIES (for which the programmer will obviously not respond).

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

Java is pretty good actually, if you have the proper programming methods in place - and your requirement (a high integrity system) is interesting enough - this is a much bigger problem with the programming methodology (unit tests, tons of internal tests, multiple instances in parallel comparing the results - how space shuttle control computers - in case there is one malfunction) than what the language solves.