Re: If not Ada, what else...

["Dmitry A. Kazakov" <mailbox@dmitry-kazakov.de>]

On Sat, 11 Jul 2015 09:51:07 +0200, Georg Bauhaus wrote:

> On 11.07.15 04:31, Paul Rubin wrote:
> 
>> Historically AFAIK range types in Ada were not statically checked.
>> Checking them is very complicated and can be partly automated these days
>> with SMT solvers, but in general you'd need proof assistants and lots of
>> manual effort.
> 
> The expressly bounded, named types of Ada to me are fundamental to sorting
> things out. In many ways, for example: how could one find a function
> from integers into integers to be from N -> {0, 1, ..., 10}, actually,
> if there was no better way to specify the set of values in a type than
> by saying "int"? Knowing more about the sets continues transitively, and
> this knowledge is reflected in the definitions of user defined fundamental
> types (with ranges etc.).

Partially. Ada 83 didn't make it fully static, because it disregarded
operations. It is not enough to declare a range or, more generally, the set
of values to define a type. Because type includes operations. E.g. the
numbers 1..10 may not have unary minus, as they don't have inverses.

What Ada 83 did to resolve the problem was less typing. It relaxed
contracts to uphold them. Constraint_Error was added to the contracts of
all operations. Ada simplified issues with intermediate results by making
them of the base type (C used type promotion for this). This was a
compromise, but compromises never win.

-- 
Regards,
Dmitry A. Kazakov
http://www.dmitry-kazakov.de