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.