Programming languages for a safe and secure future

[Hannes Mehnert]

-----BEGIN PGP SIGNED MESSAGE-----
Hash: SHA384

Hey,

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).

Still, we can do better.

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/)

There are certain tradeoffs and minor differences between those, I
have the most hope with idris at the moment (due to design decisions
from a practical point of view).

In the end, I hope that the dream of (at least partially) verified
systems will be reality during my lifetime,

Hannes
-----BEGIN PGP SIGNATURE-----
Version: GnuPG v2.0.19 (FreeBSD)

iQIcBAEBCQAGBQJS3BUAAAoJELyJZYjffCjuF5MQALL5PqQyUYWH7TJQn6ZD3FwR
vk/7OZwvlt2InHjFq1sx6mMp+k4/7Dc2Eb32rUPukU5NYIgmoIVGQz5rc3tTUUMH
T8ttcjD8VP95Px26X3Gw3v9rD8QlWSUUdPtjC4IFK0lDhLmMzQDy49IPrh72XtEv
GNZogxS29swhajhgh0UUieGoUnL55BafGnZoYu6j10OfY1qEsnLH++ISHM+G0HtS
rOoi6dAlDW2wAj8Z6FopkWlTBuGjBeZD+csgg3y6r8LYRDKnl0KBcngdkHKjQ1UV
UrqyYDiTOr2EG8ddYua7ZK756TdBDLVmsl5Er3KZFIaoY3D6QHvMbRd0NTNkSUJh
yOqLS4RVlF22ztRKhn9oKTSyGRWRBIJCCPu7RPSHxs4fHJUfyRo1I2zI2RLaFNbU
V5CYiS++EFgM+EyljcjoC5oYrjlEKA8lOAAgeaS0XJA1ViqnPo8BMsza50DLq7MS
/MgWzSw8x43Ph4wjdeZwAH2XjM8Ek9SKXp+ojm61poYse2SWllfPyIZZOlDsAAgO
Z0gjtZCFPVCEhoCTuSIULIJBQfcNkIoZw7feREwMYyV1bIdsOSjUC6bAIf6tmDB9
pkjO8jmyFC1B0GNeTBaLpIhcjdxtHz8xHi0f5U6uygt+pDZgCls7Xs3GgAWCoVHu
e8+/2nfYpatyqDzmlkRh
=Qz7b
-----END PGP SIGNATURE-----