[glossing over C and C++ lumped together; if there's one implementation that's seen exhaustive scrutiny, it would be Bitcoin in C++. only DJB can write C code without harm at every corner, however! ;]
On Sun, Jan 19, 2014 at 10:43 AM, Hannes Frederic Sowa <[email protected]> wrote: > ... > Maybe you can comment a bit on the code extraction process into compilable > languages. > > There seems to be a semantic differences between the proofable > language and the language the extraction process targets in e.g. array > handling(e.g. ocaml code) or just overflow handling in integers. > I guess Idris does not have this problem? > > I always wondered if ats-lang would be the most suitable language for > writing more typesafe code? thank you for these pointers, learning new things++ related efforts i've found interesting: Quark, ProofWeb, Frama-C, ELFbac, and interesting 30C3 presentation on "bug class genocide" http://www.youtube.com/watch?v=2ybcByjNlq8 best regards,
