Re: If not Ada, what else...

[Georg Bauhaus <bauhaus@futureapps.invalid>]

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.). They also match the problem description.

In C, when a function returns negative, this typically means one of the
known errors, or about |0 - INT_MIN| possible cases of overflow or worse.
How do we learn about the image that the function was supposed to compute?
Read comments? Studying the full source?

The existence, and perhaps proliferation of fusion into Haskell programs
OTOH turns them into mathematical riddles. I wonder if that's just what
fans of Haskell might like doing? Turning some simple Haskell equations
into fusioned somethings for reasons of *controlling* performance in time
vs space, which, IIUC, were not part of Haskell's design. They are not an
integral part of its expressive apparatus. (Sadly.) So we get to see
efficient manipulations of data in Haskell using all kinds of primitives
and strict so that code looks just like some kind of new, operation-
oriented  assembly language, using a fancy equational machine.

> Embedded is a niche,

I understand that embedded covers about half of the market of all
things that have computers in them. I don't know whether that's
money-wise or installation-wise.  Perhaps awareness isn't half, too.