[spitfire]

These sort of articles (and the attendant comments about false positives) always scream out for Ada to me. It's a language designed by a calm, careful thinker back in the 80's for life critical programs. It has everything Java and C++ have except the vast number of undefined states and it's designed for static analysis. By designed I mean, there are formal verifiers and the NSA has used it in a test security system.

Plus the compiled code is pretty fast. So if you're feeling the need to reduce your workload take a look at it, you might be surprised.

[cageface]

What kinds of libraries are available for Ada? Half the reason I use C++ is that half the code I need to write is already available in mature libraries.

[spitfire]

Library support is aimed squarely at realtime life critical systems. You're more likely to find a library with some sort of safety certification than not. If you're expecting to use the latest web libraries or hadoop you'll be disappointed.

However, there is a small collection of oss Ada libraries out there.

[axman6]

I seem to remember there was a pretty interesting web framework written in Ada, Adaweb I think?

Anyway, Ada has some other amazingly cool features. The concurrency primitives it offers are very cool, lets you make some much stronger guarantees about the interactions between threads than any other language I've seen. For example, you can define rendezvous sections, which if memory serves, are pieces of code that are guaranteed to only be run once both threads participating in the rendezvous and neither thread can leave the section until both are ready.

[spitfire]

There's ada web server (aws) which is neat. Similar idea to the java web kits like jetty. You can even hotplug code during runtime.

You're right about the concurrency. Ada has a bunch of stuff like that built into the language since 1983.

The particularly cool toys I like are SPARK (a formal verifier tool) and stackcheck - tells you exactly how deep in the stack your code can possibly go. (Yes you have to annotate cycles.)

[iskander]

Admittedly I only programmed in Ada for a few months, but I found it to be an unbearably tedious language. The verbosity is monstrous--- the type system is inexpressive; it feels primitive. Nothing is inferred, everything is repeated. Ugh, I would rather code exclusively in C++ templates than touch Ada again.

[spitfire]

I will freely admit that Ada is not appropriate for all uses. But for the sort of thing you'd want to use Ada for (life critical systems, critical infrastructure, control systems, etc) The explicit type system, explicit declaration, statically typed system is ideal. I particularly like the ability to declare down to the bit level how my data is stored. Very useful for working with low level hardware.

Take a look again, with an eye towards large scale long lived critical systems. You'll find that explicitness a feature, as is the very strict static typing.

Oh, and they got pointers right the first time.

EDIT: Forgot to mention the coolness of the type system - you can declare ranges and other type information and the compiler will hold that requirement strictly. for example type direction is range 0..359; Declares the obvious, but now you can have the compiler error if you assign a direction type with a value that might be outside that range. Even if you don't set that option you can always use the foo'valid attribute to check that foo is within bounds. This is used to check for stray cosmic radiation (seriously!).

Yes it seems like overkill. But when you come back to 20 year old code that's still running you'll smile.

[protomyth]

I would also add that Ada compilers do generate some surprisingly efficient executables. This helps quite a lot in the embeded space.