It is the output of ISO WG13 so you have to buy the (very) expensive ISO standard if you want to play with it. However, there are several compilers still available which implement ISO M2. Personally I don't like their choice of syntactic sugar, but I can see why they did things. I subscribed to another M2 dialect. By the time the full spec was published most industrial people had moved to other languages for purely commercial reasons.
The specification is in VDM-SL which can be checked by software tools. It isn't very easy to read though. A small piece is online as an example and is a bit out of date but gives the flavour.
AFAIK it is one of only a handful of non-trivial languages with a complete formal language specification that has been machine checked.
Some problems with the Viper chip showed that hardware struggles with formal proof of correctness too.
Some of the better static analysis tools for Modula2 can see into the program and find very deep faults that would not be found in normal execution. Apparently reliable working libraries were found to have a few flaws when the most successful static testing tools became available.
Halting problems are notoriously difficult.
No. Although I was never a great fan of Ada.
I think it was John Barnes at Praxis that did the high integrity stuff.
It is a common misconception that Lisp is always interpretted. I was involved long ago in the development of a Common Lisp Compiler. There are incremental Lisp compilers which may look from the outside like interpretters but generate fast native code. The whole compiler and its libraries was written in Lisp and bootstrapped with a Lisp interpretter onto new hardware. Only the deepest layer of OS interface was done in assembler it ran on the Mac and later on the PC.
OS/2 was pretty good in this respect. Step out of line and your process gets swatted before it can do any harm.
Limiting address range each process is allowed to access will do.
You do have to be careful you don't create something that is unweildly. x86 has an array BOUND instruction but I can't recall ever seeing it used in anger. The Modula2 solution was to have pragmas that allowed development code to insert preambles and postambles to defend against stack overflow, numeric faults, page faults etc and a kernel to return a traceback or postmortem dump that would identify the failing code. The traceback still worked in prodcuction code but the testing was disabled.
The first PC compilers with these capabilites were around in the mid
1980's distributed by Logitech (now better know for its mouse).Regards, Martin Brown
** Posted from