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
X-Google-Thread: 103376,ad06d2d7cb045687
X-Google-NewGroupId: yes
X-Google-Attributes: gida07f3367d7,domainid0,public,usenet
X-Google-Language: ENGLISH,ASCII-7-bit
Received: by 10.68.135.231 with SMTP id pv7mr4319706pbb.8.1328260324829;
        Fri, 03 Feb 2012 01:12:04 -0800 (PST)
Path: 
 lh20ni255263pbb.0!nntp.google.com!news1.google.com!news.glorb.com!feeder.erje.net!news.mb-net.net!open-news-network.org!aioe.org!.POSTED!not-for-mail
From: "Dmitry A. Kazakov" <mailbox@dmitry-kazakov.de>
Newsgroups: comp.lang.ada
Subject: Re: Silly and stupid post-condition or not ?
Date: Fri, 3 Feb 2012 10:11:22 +0100
Organization: cbb software GmbH
Message-ID: <143dxzgfasd4o$.a7lekw80xee2$.dlg@40tude.net>
References: <op.v8w6ptk5ule2fv@douda-yannick>
 	<82wr86fzos.fsf@stephe-leake.org>
 	<5af407fc-2868-44ca-84d2-c51a2a64104d@o4g2000pbc.googlegroups.com>
 <82k445fu9n.fsf@stephe-leake.org> <jgfjc4$u4b$1@munin.nbi.dk>
Reply-To: mailbox@dmitry-kazakov.de
NNTP-Posting-Host: FbOMkhMtVLVmu7IwBnt1tw.user.speranza.aioe.org
Mime-Version: 1.0
X-Complaints-To: abuse@aioe.org
User-Agent: 40tude_Dialog/2.0.15.1
X-Notice: Filtered by postfilter v. 0.8.2
Content-Type: text/plain; charset="us-ascii"
Content-Transfer-Encoding: 7bit
Date: 2012-02-03T10:11:22+01:00
List-Id: <comp.lang.ada>

On Thu, 2 Feb 2012 21:13:04 -0600, Randy Brukardt wrote:

> I've always hated the emphasis on completeness of these things, because it 
> is *exactly* the wrong approach to getting something in wide-spread use 
> (even in the Ada community).

Putting my hat of logicians on: you can't get anywhere without
completeness. This is how logical inference rules work. Sorry for that, but
there is no other way.

The approach should be of course to have clear boundaries between provable
and non-provable parts and letting the programmer to "give his word" for
the gaps to be filled. I.e. to have *conditional* proofs.

It is very sad to see how Ada 2012 messes things up, alas.

-- 
Regards,
Dmitry A. Kazakov
http://www.dmitry-kazakov.de