Re:Why Ada Is the Language You Want to Be Programming Your S...
by johnisgood on Wednesday September 18, 2019 @09:09PM
(#21012225)
More information about Get_Line: https://blog.adacore.com/formal-verification-of-legacy-code
That's perhaps an oversimplification; elsewhere it's been said of Ada's mentality that "Incorrect Is Simply Not Allowed." — but there's ALWAYS been a preference for pushing checks from dynamic to static, and from runtime to compile-time.
As a trivial example, the following code is typically generated without any sort of index check because the loop-control variable takes its range from the Array, it's obvious that it CANNOT be an invalid index, and this is allowed by the language reference manual (and encouraged by the annotated reference manual)—
Conversely, there are places where you cannot statically determine the validity: