Re: A function that cannot be called?

["G.B." <bauhaus@notmyhomepage.invalid>]

On 20.10.18 03:34, Randy Brukardt wrote:
> "G.B." <bauhaus@notmyhomepage.invalid> wrote in message
> news:pqco17$2vr$1@dont-email.me...
> ...
>> The members of the functionist faction will turn their eyes
>> towards the cieling in dispair:
>> it is these weird functions involving uninhabited types that have
>> turned out to be essential for the interplay between logicians
>> and computer scientists discovering practical solutions. For
>> example, what about a type system that guarantees termination?
> 
> It's this sort of babble that makes me want to ignore formal models of
> anything and just get my freaking work done. :-)

The lucid clarity of the (A)ARM speaks for itself...

It might wet your appetite to recall that without the formal model
of classical logic, none of Ada or its RM would be used by us.

The safe SPARK subset of Ada cannot exist without type based
static program analysis. SPARK is largely based on the above babble.
No less.

Note also that "discovery" is meant as "result of working on
properties and effects of programming language designs"
in research. Results such as not being able to introduce certain
bugs into a program text because compile time type analysis
can then proove absence of termination bugs.  Sounds familiar,
doesn't it, almost like taken from a SPARK brochure.

Granted, the ink spot habits of functionists' writing style
is incompatible with Ada culture. But they are mathematicians
in disguise and so will push their guild's symbolism. 8->