asciilifeform: i'ma cheat and cite my own article, http://www.loper-os.org/?p=1913 : '... in a heavily-restricted subset of the Ada programming language — the only currently-existing nonproprietary statically-compiled language which permits fully bounds-checked, pointerolade-free code and practically-auditable binaries. We will be using GNAT, which relies on the GCC backend.'
asciilifeform: i did not do it because it adds runtime overhead ( the bounds get checked , and even in inner loops ) without preventing any kind of problem that can happen in reality
asciilifeform: i had it set to max fascism. which explains why bounds of same item get checked again and again and again and...
asciilifeform: ada is interesting because 1) all array accesses boundschecked. you CAN hardwarize this. but also 2) whole program is forced to conform to strict rules, said conformance can only be evaluated during compilation, and strictly when taken as whole
asciilifeform: 90% of why i like ada is that it 'compiles like c' (i.e. without massive runtime or bytecode claptrap in place of ida-able binary) WHILE having bounds-checked array accesses etc.
asciilifeform: (i loathe ada, but this needs a BOUNDS-CHECKED language where i can AUDIT THE BINARY and NO RUNTIME COMPONENT / GC - which leaves exactly ONE)