Programming languages for a safe and secure future

[Hannes Frederic Sowa]

Hi Hannes! :)

On Sun, Jan 19, 2014 at 06:10:08PM +0000, Hannes Mehnert wrote:
> On 01/18/2014 23:29, coderman wrote:
> > other languages on my short list: - C/C++ (it's everywhere.  it
> > will remain everywhere.) - Scheme/Lisp (for the perspective more
> > than utility) - Ruby/PHP/PERL (good complements to Python. except
> > PHP, which should be hated and ostracized :) - Bash/Csh/PowerShell
> > (scripting++) - Go/C#/Java (you're going to want to know these
> > sooner or later) what would you add, and why?
> 
> while it is nice to see that people are interesting in programming
> language where common bug classes of C and C++ are not present (read:
> no buffer overflows, format string exploits, no memory corruptions due
> to temporal safety (no double free etc.)). I suggest to look into
> http://media.ccc.de/browse/congress/2013/30C3_-_5412_-_en_-_saal_1_-_201312271830_-_bug_class_genocide_-_andreas_bogk.html
> - -- which is about a compiler plugin to get rid of these bug classes in
> C (or any other language using LLVM).

MPX was already committed to gcc trunk, so I hope this situation could
improve in future (it is reverted for 4.9 but I think it will come back
after the release in March).

(I am still not sure how this will be rolled out, maybe by switching
some software back to 32 bit to reduce the load on the pointer length
lookup tables.)

> The rise of the Curry-Howard correspondence (programs and proofs are
> the same!) resulted in several programming languages whose type
> systems are so expressive that it can carry mathematical proofs (of
> intuitionistic logics) around. The common hello-world example is a
> list carrying (at compile time!) its length around, and thus being
> able to verify that append called on a list of length n and a list of
> length m returns a list of length n + m (and that reverse returns a
> list of the same length).
> 
> While it is true, that these examples and languages are used mainly in
> computer science at the moment, I hope to see more people attracted to
> these kind of languages, writing libraries and applications.
> 
> I can recommend several languages:
>  - coq (http://coq.inria.fr) [the tutorial software foundations
> http://www.cis.upenn.edu/~bcpierce/sf/ ]
>  - agda (http://wiki.portal.chalmers.se/agda/pmwiki.php)
>  - idris (http://www.idris-lang.org/)

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?

Greetings,

  Hannes