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: border2.nntp.dca1.giganews.com!buffer2.nntp.dca1.giganews.com!border2.nntp.dca3.giganews.com!backlog4.nntp.dca3.giganews.com!border2.nntp.dca.giganews.com!nntp.giganews.com!news.glorb.com!us.feeder.erje.net!feeder.erje.net!eu.feeder.erje.net!weretis.net!feeder1.news.weretis.net!news.imp.ch!newsfeed.tiscali.ch!npeer.de.kpn-eurorings.net!npeer-ng0.de.kpn-eurorings.net!newsfeed.arcor.de!newsspool2.arcor-online.net!news.arcor.de.POSTED!not-for-mail Date: Wed, 18 Jun 2014 16:43:55 +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> <53a15d0a$0$6619$9b4e6d93@newsspool4.arcor-online.net> <1f63h2p39u7oi$.tj7uwc9s8i68.dlg@40tude.net> In-Reply-To: <1f63h2p39u7oi$.tj7uwc9s8i68.dlg@40tude.net> Content-Type: text/plain; charset=ISO-8859-1; format=flowed Content-Transfer-Encoding: 7bit Message-ID: <53a1a5ab$0$6654$9b4e6d93@newsspool3.arcor-online.net> Organization: Arcor NNTP-Posting-Date: 18 Jun 2014 16:43:55 CEST NNTP-Posting-Host: 970ab794.newsspool3.arcor-online.net X-Trace: DXC=Qa[Ld\CHDNcFXUDVUnEXQmMcF=Q^Z^V3h4Fo<]lROoRa8kFjLh>_cHTX3jmdj2fAghA:`l X-Complaints-To: usenet-abuse@arcor.de X-Original-Bytes: 3884 Xref: number.nntp.dca.giganews.com comp.lang.ada:187051 Date: 2014-06-18T16:43:55+02:00 List-Id: On 18.06.14 14:30, Dmitry A. Kazakov wrote: > On Wed, 18 Jun 2014 11:34:01 +0200, G.B. wrote: > >> (Pardon? A contract is a manifest piece from the equivalence >> class of paper, signed by two parties. > > And that does not defines the parties it only constrains them, which was > the point. In fact, you declared "contract" to be a "framework of constraints imposed on the implementations" which a contract between two legal parties is not. If things required entail things constrained, then making it sound as if this was an equality, or even the other way around is invalid. There is then nothing that warrants mentioning Hilbert. Maybe if the two parties have agreed to stop programming entirely in view of of Hilbert's program. >>> 2. You cannot have exhaustive contracts. >> >> Writing contracts is not a just formal logic, it is about >> programmers *behaving* responsibly when programming: > > Irrelevant. Essential because behavior of parties is the subject of court rulings. If it is found that for whatever reason the contract was violated by programmer X, then programmer X can be held responsible. This is true even in case some technical detail seems to contradict at the source level. ("It is found" outweighs formal logic.) > If you are contracted to smoke one block a day, that might be irresponsible > on your side, but a contract is a contract. If I sign a contract with you about doing X, and then I don't do X, then you can hold me responsible. Whether or not I actually didn't do X is the matter that a compiler cannot always decide, but courts will. Whether or not some Y finds doing X morally irresponsible WRT Y's frame of reference is indeed irrelevant if Y is not the court.