Re: A function that cannot be called?

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

On 20.10.18 13:13, Simon Wright wrote:
> "G.B." <bauhaus@notmyhomepage.invalid> writes:
> 
>> 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.
> 
> *whet
(Ah. Thank you.)
> Who is "us"? Certainly doesn't include me.

The idea is that classical logic caused, and continues to cause,
(features of) programming languages like Ada, in some sense.
The idea is not to suggest that programmers need to be concerned
with formal models in order to write programs.

So, I guess for writing an embedded program like

   loop
     Ouput (Compute (Input));
   end loop;

one doesn't need to be aware that classical logic, without some
type system, incurs the possibility of the HALTing trouble.
But, OTOH, pure functionists with "program terminating types"
will need monads and things as a way to write a non-terminating
program.