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_-_2013122... - -- 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