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.9 required=5.0 tests=BAYES_00,FORGED_GMAIL_RCVD,
	FREEMAIL_FROM autolearn=no autolearn_force=no version=3.4.4
X-Received: by 2002:a6b:6807:: with SMTP id d7-v6mr3384265ioc.7.1540305353405;
        Tue, 23 Oct 2018 07:35:53 -0700 (PDT)
X-Received: by 2002:a9d:3f09:: with SMTP id m9mr900270otc.5.1540305353205;
 Tue, 23 Oct 2018 07:35:53 -0700 (PDT)
Path: 
 eternal-september.org!reader01.eternal-september.org!reader02.eternal-september.org!feeder.eternal-september.org!news.gegeweb.eu!gegeweb.org!usenet-fr.net!proxad.net!feeder1-2.proxad.net!209.85.166.215.MISMATCH!z5-v6no68965ite.0!news-out.google.com!n199-v6ni79itn.0!nntp.google.com!75-v6no69204itm.0!postnews.google.com!glegroupsg2000goo.googlegroups.com!not-for-mail
Newsgroups: comp.lang.ada
Date: Tue, 23 Oct 2018 07:35:52 -0700 (PDT)
In-Reply-To: <pqn1km$28q$1@dont-email.me>
Complaints-To: groups-abuse@google.com
Injection-Info: glegroupsg2000goo.googlegroups.com;
 posting-host=96.247.204.201;
 posting-account=QF6XPQoAAABce2NyPxxDAaKdAkN6RgAf
NNTP-Posting-Host: 96.247.204.201
References: <pq9tf7$9bf$1@dont-email.me>
 <99f41210-6fe2-4b4d-90ad-21a0ab108f53@googlegroups.com>
 <pqced4$5gl$1@dont-email.me>
 <39dec2d6-7da5-4421-bb50-e4effd5a1439@googlegroups.com>
 <pqdcvk$9v5$1@dont-email.me>
 <d8e778fb-09d0-4989-b1e0-76b3148211f5@googlegroups.com>
 <pqhjhc$5vr$1@dont-email.me>
 <104caa52-8e0b-4699-996e-74f382c31ba7@googlegroups.com>
 <pqn1km$28q$1@dont-email.me>
User-Agent: G2/1.0
MIME-Version: 1.0
Message-ID: <a25bdd7c-6ca0-4520-b1bc-c33cdaab1625@googlegroups.com>
Subject: Re: A function that cannot be called?
From: Jere <jhb.chat@gmail.com>
Injection-Date: Tue, 23 Oct 2018 14:35:53 +0000
Content-Type: text/plain; charset="UTF-8"
Xref: reader02.eternal-september.org comp.lang.ada:54696
Date: 2018-10-23T07:35:52-07:00
List-Id: <comp.lang.ada>

On Tuesday, October 23, 2018 at 7:45:27 AM UTC-4, G.B. wrote:
> On 21.10.18 13:30, Egil H H wrote:
> 
> > package What is
> >     pragma Assertion_Policy(Check);
> > 
> >     type Void is private with Type_Invariant => False;
> >     
> >     function Impossible return Void with Pre => False;
> >     
> > private
> >     
> >     type Void is null record;
> >     
> > end What;
> 
> This approach maybe illustrates a point best: in which way
> does Ada's type system support detecting errors in a program
> early? Or is is SPARK's type system? Compile time will be best.
> 
The difficulty with compile time comes from your requirements I think.
In order for the function to exist, the compiler needs to have it 
actually be callable. Since Ada was not designed with such a type in
mind, it would be difficult for the compiler to meet both requirements
at the same time.  If it were built from scratch with such a type in
mind, perhaps.