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=-1.9 required=5.0 tests=BAYES_00 autolearn=unavailable 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!weretis.net!feeder4.news.weretis.net!news.teledata-fn.de!newsfeed.arcor.de!newsspool1.arcor-online.net!news.arcor.de.POSTED!not-for-mail Date: Wed, 18 Jun 2014 11:34:01 +0200 From: "G.B." User-Agent: Mozilla/5.0 (Macintosh; Intel Mac OS X 10.9; rv:24.0) Gecko/20100101 Thunderbird/24.6.0 MIME-Version: 1.0 Newsgroups: comp.lang.ada Subject: Re: a new language, designed for safety ! References: <1402308235.2520.153.camel@pascal.home.net> <85ioo9yukk.fsf@stephe-leake.org> <255b51cd-b23f-4413-805a-9fea3c70d8b2@googlegroups.com> <5ebe316d-cd84-40fb-a983-9f953f205fef@googlegroups.com> <2100734262424129975.133931laguest-archeia.com@nntp.aioe.org> <665318547424646901.823673laguest-archeia.com@nntp.aioe.org> <53a127a6$0$6658$9b4e6d93@newsspool3.arcor-online.net> <117hu7inluueh.8yl6k6ubrlo5.dlg@40tude.net> In-Reply-To: <117hu7inluueh.8yl6k6ubrlo5.dlg@40tude.net> Content-Type: text/plain; charset=ISO-8859-1; format=flowed Content-Transfer-Encoding: 7bit Message-ID: <53a15d0a$0$6619$9b4e6d93@newsspool4.arcor-online.net> Organization: Arcor NNTP-Posting-Date: 18 Jun 2014 11:34:02 CEST NNTP-Posting-Host: d682a181.newsspool4.arcor-online.net X-Trace: DXC=GJOcfih1Y?XaAeROF2PWMQ4IUKZLh>_cHTX3j]VFXR7i:A4;W X-Complaints-To: usenet-abuse@arcor.de Xref: news.eternal-september.org comp.lang.ada:20426 Date: 2014-06-18T11:34:02+02:00 List-Id: On 18.06.14 10:02, Dmitry A. Kazakov wrote: > 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 [...] define the semantics through the > contract. Contracts are not about this illusion of exhaustive semantics. The topic (intent) of a contract is really programmer behavior. It's a legal (cf. Law, not LRM) thing. A contract does not tackle the decision problem, no matter what the formal tools will do. A contract helps Programmer B, who is a reader of the contract, finding a meaningful answer, in the contract, to the question: "What if I ...?" B doesn't expect miracles (exhaustive miracles that would be) but B's employer does expect *liability*, which is the term Jeffrey Carter has used. If B tells his employer that the entity T does not do what the contract says it does, then B's employer can talk to the supplier (who has signed the contract as the other party) and ask for corrections if they agree that B's observation is correct. They decide what's the case. > Per definition of contract, (Pardon? A contract is a manifest piece from the equivalence class of paper, signed by two parties. Don't blur the distinction by suggesting that some formal modes of expression (via Pre, Post, etc.) stand for the entire notion of contract: Townsville, 6th of December 2003 CONTRACT between Programmer A and Other Programmers We agree that entity T can be used in such a way that {... some *agreed* *upon* meaningfulness ...} Signed for programmer A for Other Programmers Programmer A John Doe (No arbitrary wikipedia links this time please, this is serious. Programming has not invented the word "contract", neither has mathematics, and since this is about programmers and other professionals as legal entities, not compilers, formalist views of "contract" are much too narrow. And also beside the point. Programming is a subordinate here.) > 2. You cannot have exhaustive contracts. Writing contracts is not a just formal logic, it is about programmers *behaving* responsibly when programming: Boss: "Sit down, and write a description of your type from which both we and they can learn what matters to the contract to be signed with Client Corp!") Programmer: "O.K., o.K., I will!" Boss: "You better had do that!" > 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. Yes! Yes! A thousand times Yes! This is what contract based design is about.