[mofosyne]

Doesn't ADA have some method of checking if the input/output of a function is within bound? Can't remember if its a runtime or compile check however.

But the concept of function contract verification would be interesting.

[carlmr]

The pre/postconditions in Ada are runtime checks [1]. GNATprove can be used to statically check these though in the SPARK subset of Ada [2].

[1] https://www.adacore.com/gems/gem-31 [2] https://docs.adacore.com/spark2014-docs/html/ug/en/source/as...