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: a07f3367d7,5add429c86f59001
X-Google-Attributes: gida07f3367d7,public,usenet
X-Google-NewGroupId: yes
X-Google-Language: ENGLISH,ASCII
Path: 
 g2news2.google.com!news4.google.com!proxad.net!feeder1-2.proxad.net!usenet-fr.net!de-l.enfer-du-nord.net!news.weisnix.org!newsfeed.ision.net!newsfeed2.easynews.net!ision!newsfeed.arcor.de!newsspool2.arcor-online.net!news.arcor.de.POSTED!not-for-mail
From: "Dmitry A. Kazakov" <mailbox@dmitry-kazakov.de>
Subject: Re: Ada vs Eiffel - Ada programmer approach
Newsgroups: comp.lang.ada
User-Agent: 40tude_Dialog/2.0.15.1
MIME-Version: 1.0
Content-Type: text/plain; charset="iso-8859-1"
Content-Transfer-Encoding: 8bit
Reply-To: mailbox@dmitry-kazakov.de
Organization: cbb software GmbH
References: 
 <405b5054-4c8f-4e16-9ea8-503a9b9f976e@t21g2000yqi.googlegroups.com>
  <4A19765C.608@obry.net>
 <8105b65f-4de9-4653-b43a-d55ee33f072d@k2g2000yql.googlegroups.com>
 <130yh6dv3l1lf$.1729u4tpolgwi.dlg@40tude.net>
 <4a1c2652$0$30220$9b4e6d93@newsspool1.arcor-online.net>
 <1r1ho3wqsjncb.1p3p7qe2qcqmw.dlg@40tude.net>
 <4a1c2dfe$0$30236$9b4e6d93@newsspool1.arcor-online.net>
 <uw2akaqgnepe$.1i0g9dauyj3x3.dlg@40tude.net> <4A1C4D9A.8010407@obry.net>
Date: Tue, 26 May 2009 23:28:47 +0200
Message-ID: <19og18pj35aqg.doeis3cu2e0e$.dlg@40tude.net>
NNTP-Posting-Date: 26 May 2009 23:28:48 CEST
NNTP-Posting-Host: 4fe20539.newsspool2.arcor-online.net
X-Trace: 
 DXC=HmAP?==Ufh4TQL:hoD@>T?A9EHlD;3Yc24Fo<]lROoR1^YC2XCjHcb9:D]QH12R7@5DNcfSJ;bb[5IRnRBaCd<M>T6NQQB3U^R6NC1]S8]HKI0
X-Complaints-To: usenet-abuse@arcor.de
Xref: g2news2.google.com comp.lang.ada:6031
Date: 2009-05-26T23:28:48+02:00
List-Id: <comp.lang.ada>

On Tue, 26 May 2009 22:14:18 +0200, Pascal Obry wrote:

> Dmitry A. Kazakov a �crit :
>> Nope, the point is not how many checks, it is about consistency of checks.
>> SPARK does it consistently, Eiffel does not.
> 
> Well SPARK and Eiffel are playing the same game at all!
> 
> SPARK imposes some very strong constraints on the developer (for good
> reasons) to build and *prove* something right.

Yes. The amount of checks and so the limitations imposed by them depends on
the word "something" you used above. You can require to prove less or more,
but never all.

Many programmers are already satisfied with much less than SPARK offers,
e.g. with strong static typing, which gives a proof of no type errors. But,
continuing this example, dynamic typing gives no such proof. Therefore it
is either not strong (most of dynamically typed language are in fact weakly
typed) or else the dynamic type checks (like dispatch in Ada) are not error
checks, but merely correct contracted behavior.

In my view run-time checks as a form of contract enforcement is a bad
practice, which makes the programmer believe in safety that does not exist.
Instead of that he should consider his design to define the behavior for
the cases where the "contract" can be violated, making a new contract that
is never violated and thus requires no checks.

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