23 ms·

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

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.

dalke 11y ago
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.
iamcurious 11y ago
You mean at compile time? Could you explain how or point me to some references?
- krapht 11y ago
  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.
  - iamcurious 11y ago
    Interesting. Thanks! (For a moment I thought the comment had a typo and was actually referring to Agda.)
Dewie3 11y ago
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?
- david-given 11y ago
  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.

dalke 11y ago

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.

iamcurious 11y ago

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

krapht 11y ago
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.
- iamcurious 11y ago
  Interesting. Thanks! (For a moment I thought the comment had a typo and was actually referring to Agda.)

Dewie3 11y ago

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?

david-given 11y ago
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.