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!news.eternal-september.org!mx02.eternal-september.org!feeder.eternal-september.org!aioe.org!.POSTED!not-for-mail
From: "Nasser M. Abbasi" <nma@12000.org>
Newsgroups: comp.lang.ada
Subject: Re: Haskell, anyone?
Date: Sun, 15 Nov 2015 23:59:27 -0600
Organization: Aioe.org NNTP Server
Message-ID: <n2brc1$kg0$1@speranza.aioe.org>
References: <c6ac0d2f-52af-4aa6-ba6f-34f61e3c93e8@googlegroups.com>
 <dd1ada14-493d-44fc-a081-3a69515f2702@googlegroups.com>
 <n2b23f$aom$1@speranza.aioe.org> <87mvue50ey.fsf@ixod.org>
 <87d1vaoa6y.fsf@nightsong.com> <n2bosk$gsq$1@speranza.aioe.org>
 <878u5yo5p9.fsf@nightsong.com>
Reply-To: nma@12000.org
NNTP-Posting-Host: xsLQkk658PrKN3IVMCswbw.user.speranza.aioe.org
Mime-Version: 1.0
Content-Type: text/plain; charset=windows-1252; format=flowed
Content-Transfer-Encoding: 7bit
X-Complaints-To: abuse@aioe.org
User-Agent: Mozilla/5.0 (Windows NT 6.1; WOW64; rv:38.0) Gecko/20100101
 Thunderbird/38.3.0
X-Notice: Filtered by postfilter v. 0.8.2
Xref: news.eternal-september.org comp.lang.ada:28390
Date: 2015-11-15T23:59:27-06:00
List-Id: <comp.lang.ada>

On 11/15/2015 11:48 PM, Paul Rubin wrote:
> "Nasser M. Abbasi" <nma@12000.org> writes:
>> It is detected at compile time. It gives warning. So compiler
>> can see at compile time the problem.
>
> That's different, a special case that the compiler happens to be able to
> figure out.  A true compile time check will refuse to compile the code
> unless it can prove x+y<20, possibly with manual assistance.

But the source code is legal. So it has to compile it. But
it does give a warning. In Ada, the practice is to keep working
on the code until one gets a clean compile. By clean, it means
no warnings.

I think we are arguing about semantics here. For me, the compiler
did detect this at compile time, and issued a "message" to the user.
That was the point.

> Also the
> lack of proof would result in an error (you can't compile the code), not
> a warning.
>

Again, I am not a programming language lawyer. But legal code
should compile. Error should be generated only if the code is
not confirming to the standard. So I do not think this should be
an "error" but only a  "wanring".

--Nasser