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!news.eternal-september.org!news.eternal-september.org!feeder.eternal-september.org!aioe.org!.POSTED!not-for-mail
From: "Dmitry A. Kazakov" <mailbox@dmitry-kazakov.de>
Newsgroups: comp.lang.ada
Subject: Re: a new language, designed for safety !
Date: Wed, 18 Jun 2014 10:02:03 +0200
Organization: cbb software GmbH
Message-ID: <117hu7inluueh.8yl6k6ubrlo5.dlg@40tude.net>
References: <lmj8s6$hhp$1@speranza.aioe.org>
 <1402308235.2520.153.camel@pascal.home.net> <85ioo9yukk.fsf@stephe-leake.org>
 <ln6tlg$1vc$1@dont-email.me>
 <255b51cd-b23f-4413-805a-9fea3c70d8b2@googlegroups.com>
 <ln6uv9$bk8$1@dont-email.me>
 <b22db9fb-a73d-438a-8cfd-f0bb1db70eed@googlegroups.com>
 <MPElv.491358$1w1.428312@fx03.iad>
 <5ebe316d-cd84-40fb-a983-9f953f205fef@googlegroups.com>
 <ln7ngt$c8a$1@dont-email.me>
 <2100734262424129975.133931laguest-archeia.com@nntp.aioe.org>
 <lnn5ko$ner$1@loke.gir.dk>
 <665318547424646901.823673laguest-archeia.com@nntp.aioe.org>
 <lnnt1g$mka$1@dont-email.me> <lnpdt2$ggn$1@dont-email.me>
 <lnq5kj$e2v$1@loke.gir.dk> <lnq78k$ur8$1@dont-email.me>
 <53a127a6$0$6658$9b4e6d93@newsspool3.arcor-online.net>
Reply-To: mailbox@dmitry-kazakov.de
NNTP-Posting-Host: QTaafVZuunHujkJPndFR7g.user.speranza.aioe.org
Mime-Version: 1.0
Content-Type: text/plain; charset="us-ascii"
Content-Transfer-Encoding: 7bit
X-Complaints-To: abuse@aioe.org
User-Agent: 40tude_Dialog/2.0.15.1
X-Notice: Filtered by postfilter v. 0.8.2
Xref: news.eternal-september.org comp.lang.ada:20424
Date: 2014-06-18T10:02:03+02:00
List-Id: <comp.lang.ada>

On Wed, 18 Jun 2014 07:46:13 +0200, Georg Bauhaus wrote:

> Unfortunately, Ada 2012 makes the contractual aspect of
> programming an optional part, and in some pinboard style list of
> notes at that.

1. You cannot contract everything, i.e. define the semantics through the
contract. Per definition of contract, it is a framework of constraints
imposed on the implementations (many).

2. You cannot have exhaustive contracts. That is per the nature of things
(e.g. the Hilbert's program).

1+2. There are many possible contracts, there always exist implied
contracts. Thus you should not require an explicit contract provided the
implied one is OK.

My dream is an ability to start with minimal proofs and, as the program
matures, to add checks later, incrementally. That would be a sort of better
TDD (test-driven design). It would keep up-front design reasonably small,
which is important while requirements are unstable. You would cover the
cases either with proofs or with tests, both incrementally.

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