From mboxrd@z Thu Jan  1 00:00:00 1970
X-Spam-Checker-Version: SpamAssassin 3.4.4 (2020-01-24) on polar.synack.me
X-Spam-Level: 
X-Spam-Status: No, score=-0.3 required=5.0 tests=BAYES_00,
	REPLYTO_WITHOUT_TO_CC autolearn=no autolearn_force=no version=3.4.4
Path: 
 eternal-september.org!reader01.eternal-september.org!reader02.eternal-september.org!.POSTED!not-for-mail
From: "G.B." <bauhaus@notmyhomepage.invalid>
Newsgroups: comp.lang.ada
Subject: Re: A function that cannot be called?
Date: Sun, 21 Oct 2018 11:07:17 +0200
Organization: A noiseless patient Spider
Message-ID: <pqhfk6$gks$1@dont-email.me>
References: <pq9tf7$9bf$1@dont-email.me>
 <7ab688d0-b6b8-459c-b5b7-39b6c35daad2@googlegroups.com>
 <pqanbb$hl5$1@dont-email.me> <pqau10$us1$1@franka.jacob-sparre.dk>
 <pqco17$2vr$1@dont-email.me> <pqe0n7$1tg$1@franka.jacob-sparre.dk>
 <pqermh$r98$1@dont-email.me> <ly5zxwlvky.fsf@pushface.org>
Reply-To: nonlegitur@notmyhomepage.de
Mime-Version: 1.0
Content-Type: text/plain; charset=utf-8; format=flowed
Content-Transfer-Encoding: 7bit
Injection-Date: Sun, 21 Oct 2018 09:07:18 -0000 (UTC)
Injection-Info: reader02.eternal-september.org;
 posting-host="84d535c74bf77e66f2d335d51b8e2cb7";
	logging-data="17052"; mail-complaints-to="abuse@eternal-september.org";
	posting-account="U2FsdGVkX1+LhstSHhQoePO1Rq+Jng2MGOQ6Us9UVnw="
User-Agent: Mozilla/5.0 (Macintosh; Intel Mac OS X 10.13; rv:52.0)
 Gecko/20100101 Thunderbird/52.9.1
Cancel-Lock: sha1:7oFn7gPC1A0UAR/Hph/JOcZc3+w=
In-Reply-To: <ly5zxwlvky.fsf@pushface.org>
Content-Language: de-DE
Xref: reader02.eternal-september.org comp.lang.ada:54676
Date: 2018-10-21T11:07:17+02:00
List-Id: <comp.lang.ada>

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.