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