Programming languages for a safe and secure future

[coderman]

[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 at 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,