[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 <hannes@stressinduktion.org> 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,