High Level Programming Languages

When is it appropriate to use a high level programming language? Personally, I always feel guilty when using anything except C.

>>4

But just because the language prevents you from shooting yourself in the foot at a memory level, it doesn't mean you'll code any more securely. You can still make errors in the logic itself.

Yes, but in a higher level language (at least in one that isn't shit), you can hope that the added expressiveness will eliminate redundancy, thus allowing you to better concentrate on the logic. Logic errors are also easier to notice than accidental off-by-ones or footnote-of-manpage errors.

Furthermore, the best way to maintain security is to reduce or avoid complexity. There isn't a fundamental flaw in their translation, and any exploitation of programs in such a language relies more on the Operating System itself. Compare that to Java and its VM.

Not necessarily. JVM is a great example of how not to do anything, so bringing it up is pointless. As for complexity, most [s]Lisp[/s] anything interpreters out there are far far simpler than clang or, god forbid, gcc. My ideal platform would be one in which code is by default interpreted, and sometimes JITted into native code which is then checked by a static checker (which should be an easier problem than the usual halting-complete version since the JITC will only output a very specific subset of the possible ``native code'' programs).

>>5

Then test systems for that. Valgrind, cgdb, DynamoRIO, etc.

They're imperfect. So far automatic theorem provers aren't strong enough to prove the correctness of sufficiently-large-to-be-useful programs, so they give up on exploring beyond certain branching points.

However, Dependently typed languages

Those are horrible and you know it.