I didn't see anything about "Why Ada" other than hearing that it was useful for high-assurance RTOS, and that it has a Pascal-like syntax. Did I miss it?
Ada has the ability to verify that logic will never produce values that are unexpected. Not just "this will never be null" but something like "this number will always be between 0 and 3". That's one very nice, very different thing.
At run time - the language has built in support for assertions (syntax and conciseness way more convenient than C++ et al), contracts pre and post-condition, and you can run a formal logic analyzer on it if you limit yourself to the Spark Ada subset.
Such runtime asserts[1] are so conceptually simple though -- have enough language constructs to express invariants in the right places, and let the compiler insert asserts in all places where they would be needed. And then perhaps also have pragmas for turning off asserts for more performant but less secure builds of the code. Maybe with custom granularity for what asserts to turn off.
It's too bad that more mainstream languages don't have things like this (except for vanilla `assert` I guess). I would prefer this to something like built in unit tests.
[1] I'm assuming you are not talking about static verification, which I guess would use Spark?
Ada's contract stuff is a bit more sophisticated than a simple assertion. You can, for example, do this:
procedure increment(v: in out integer)
with
post => v /= v'old
...
(/= is Ada's not-equal-to operator.) This enforces as a postcondition that the value of v must have changed. You can even refer to the old versions of arrays.
Plus, the run-time type checking required by more complex type expressions are augmented by compile-time checking. If the compiler can deduce that a conversion will always be correct, it won't emit a check. If it can deduce that it will always be wrong, it'll error out at compile time.
It all works really rather well.
The only trouble I have with preconditions and postconditions is that you have to declare them in your module's interface, which is public, rather than in the module's implementation, which isn't. So you can only test your module's public interface. If your module doesn't expose a state variable to the outside world, you can't use it in a precondition or postcondition. I find that a very odd design decision.
You're supposed to just statically allocate memory, which is probably adequate for many special-purpose applications. There are alternative solutions, though. Some compilers offer GC, but most people use manual dynamic allocation.
- really nice strict typing (you can define a type which represents an number which varies between two values which are not known at compile time and the compiler will enforce it. And then you can define an array with it as an index, and it'll just work).
- fully nested everything with seamless upvalues. First class support for nested functions makes a lot of things easier.
- amazingly nice, rendezvous-based, type-safe message-passing concurrency. Think Go channels, but better.
- full support for generics. (e.g. the standard complex number library is supplied as a generic package so you get to specify what number type you want it to use.) There's a standard genericised container library.
- sanitised pointers. It's actually syntactically invalid to leak a pointer from an inner scope to an outer one.
- full OO support (although it's been shoehorned a little uncomfortably into the syntax; they should have added some more keywords).
- full low-level control over structure layout. You can specify the meaning of every bit of a structure, if you want (including, IIRC, endianness). If you want to.
- built-in support for design by contract. Most things you can specify preconditions and postconditions, and the compiler will enforce them.
- really fast. Like, about the same as a good C++ compiler.
The tl;dr is: fully compiled, old school systems language with rather antiquated syntax but an amazing feature set.
Plus there's the ravenscar profile for working with hard real-time systems, making it possibly the best language for working with embedded and safety critical systems.
If only the tooling was a little better (as mentioned above), Ada would be my go-to language of choice.
What sort of tooling were you looking for? I'm happy enough with gprbuild, gdb and the command line tools; I tried GNAT GPS for a bit and loathed it on sight.
No it is not nearly as nice as Haskell. It is however usable in contexts where Haskell will get people killed and on embedded devices where you can reasonably afford the Haskel overhead.
Also I haven't seen design by contract as enforced by the compiler in Haskell yet (not this is different from testing).
Any time I look at Ada I end up at AdaCore and remember how ridiculously expensive it is to work with Ada. It's almost like all the free and/or open source Ada stuff was designed to drive you to AdaCore to spend spend spend. This lack of a high quality full set of compilers and tools always reminds me why I never play around with Ada.
To me, when pricing is "get a quote", that translates to "it's so exorbitant we are afraid to put it up publicly lest people immediately be turned away before we can deliver our sales pitch".
AdaCore's compilers are lawyerbombed; they're GPL'd without the library exception, so you can't use it for non-GPL'd software. (The binaries are unreleasable due to license conflict.)
It's actually freeer to download the FSF-distributed version, which is GPL'd with the library extension. See: http://www.getadanow.com/
The FSF version is usually a couple of minor releases behind the AdaCore version, but is otherwise much less hassle.
32 comments
[ 3.1 ms ] story [ 78.6 ms ] threadIt's too bad that more mainstream languages don't have things like this (except for vanilla `assert` I guess). I would prefer this to something like built in unit tests.
[1] I'm assuming you are not talking about static verification, which I guess would use Spark?
Plus, the run-time type checking required by more complex type expressions are augmented by compile-time checking. If the compiler can deduce that a conversion will always be correct, it won't emit a check. If it can deduce that it will always be wrong, it'll error out at compile time.
It all works really rather well.
The only trouble I have with preconditions and postconditions is that you have to declare them in your module's interface, which is public, rather than in the module's implementation, which isn't. So you can only test your module's public interface. If your module doesn't expose a state variable to the outside world, you can't use it in a precondition or postcondition. I find that a very odd design decision.
- really nice strict typing (you can define a type which represents an number which varies between two values which are not known at compile time and the compiler will enforce it. And then you can define an array with it as an index, and it'll just work).
- fully nested everything with seamless upvalues. First class support for nested functions makes a lot of things easier.
- amazingly nice, rendezvous-based, type-safe message-passing concurrency. Think Go channels, but better.
- full support for generics. (e.g. the standard complex number library is supplied as a generic package so you get to specify what number type you want it to use.) There's a standard genericised container library.
- sanitised pointers. It's actually syntactically invalid to leak a pointer from an inner scope to an outer one.
- full OO support (although it's been shoehorned a little uncomfortably into the syntax; they should have added some more keywords).
- full low-level control over structure layout. You can specify the meaning of every bit of a structure, if you want (including, IIRC, endianness). If you want to.
- built-in support for design by contract. Most things you can specify preconditions and postconditions, and the compiler will enforce them.
- really fast. Like, about the same as a good C++ compiler.
The tl;dr is: fully compiled, old school systems language with rather antiquated syntax but an amazing feature set.
I did a writeup last year: http://cowlark.com/2014-04-27-ada
...and interested parties might like to see a multithreaded Mandelbrot what I wrote: http://ideone.com/a1ky4l
If only the tooling was a little better (as mentioned above), Ada would be my go-to language of choice.
Also I haven't seen design by contract as enforced by the compiler in Haskell yet (not this is different from testing).
/self goes and looks at web logs
Yikes.
And pricing on AdaCore is "Get a Price Quote." Which means, "you can afford it."
It's actually freeer to download the FSF-distributed version, which is GPL'd with the library extension. See: http://www.getadanow.com/
The FSF version is usually a couple of minor releases behind the AdaCore version, but is otherwise much less hassle.