Notes on Ada | Hacker News Reader

Notes on Ada

ada.kyleisom.net

32 pointsFractalNerve30 comments

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.

Could you elaborate on this? Are the compilers not fully-featured, or slow, or what?

Show me where to get a full set of non-GPL ADA 2012 documentation, tools, libraries, compiler, IDE, etc. that doesn't lead back to AdaCore?

And pricing on AdaCore is "Get a Price Quote." Which means, "you can afford it."

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

This book gives details on every advantage: http://www.adacore.com/uploads_gems/Ada_Safe_and_Secure_Book...

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.

Here's a detailed guide on Ada's safety-supporting features. Should help commenters wanting specifics. https://news.ycombinator.com/edit?id=9672204

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?

Isn't that enough?

I expected something more than hearsay and personal preferences, yes. Otherwise it's waste of time because those factors apply to every language.

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.

Yes, I was hoping for something which went into more of the details for when Ada might be an appropriate choice. Which is not what this link does.

You mean at compile time? Could you explain how or point me to some references?

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.

Interesting. Thanks! (For a moment I thought the comment had a typo and was actually referring to Agda.)

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.

Ada has a lot of qualities that are not given in this small article. For example, try to read the C++ standard and the Ada standard.

Now read the Haskell prologue.

Haskell has GC and lazy evaluation. It's not even relevant.

If Ada doesn't have GC, it leaks, which isn't safe.

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.

Ada's got a lot of really nice features.

- 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

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.

So it's almost as nice, and almost as safe, as Haskell.

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

That was an excellent writeup. I took the liberty of submitting it as an HN link.

Made it up to 19'th on the main page.

Thanks!

/self goes and looks at web logs

Yikes.

Reply on news.ycombinator.com