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,9e7db243dfa070d7 X-Google-NewGroupId: yes X-Google-Attributes: gida07f3367d7,domainid0,public,usenet X-Google-Language: ENGLISH,UTF8 Path: g2news2.google.com!news3.google.com!proxad.net!feeder1-2.proxad.net!news.tele.dk!news.tele.dk!small.news.tele.dk!bnewspeer01.bru.ops.eu.uu.net!bnewspeer00.bru.ops.eu.uu.net!emea.uu.net!newsfeed.arcor.de!newsspool4.arcor-online.net!news.arcor.de.POSTED!not-for-mail From: "Dmitry A. Kazakov" Subject: Re: Do people who use Ada also use ocaml or F#? Newsgroups: comp.lang.ada User-Agent: 40tude_Dialog/2.0.15.1 MIME-Version: 1.0 Content-Type: text/plain; charset="utf-8" Content-Transfer-Encoding: 8bit Reply-To: mailbox@dmitry-kazakov.de Organization: cbb software GmbH References: <87k4kz3mda.fsf@mid.deneb.enyo.de> <5jjgrklivesk$.z0is5qe7mgbt.dlg@40tude.net> Date: Sat, 30 Oct 2010 22:54:39 +0200 Message-ID: <1tglk5y57g2ci.cy0cliuo1l3d$.dlg@40tude.net> NNTP-Posting-Date: 30 Oct 2010 22:54:37 CEST NNTP-Posting-Host: 4095e733.newsspool4.arcor-online.net X-Trace: DXC=9Pc4DNG9eRI02Sh8E_NfIA4IUKH>[8M X-Complaints-To: usenet-abuse@arcor.de Xref: g2news2.google.com comp.lang.ada:15960 Date: 2010-10-30T22:54:37+02:00 List-Id: On Sat, 30 Oct 2010 22:04:34 +0200, Yannick Duchêne (Hibou57) wrote: > Le Sat, 30 Oct 2010 21:37:31 +0200, Dmitry A. Kazakov > a écrit: >>> I do not see how this could be less safe than a design process itself. >>> Generics are like building something with a pattern, and this pattern is >>> checked for consistency in Ada. >> >> So are machine instructions when executed by the processor. The argument >> is invalid: whatever does Ada with the instances of a generic body is >> irrelevant to checking the generic body. > What Ada do with generics is predictable, so you can theoretically prove > an instantiation of a generic at some point with some parameters will > fulfill some needs. No, that is a halting problem. > If I understand you correctly, you complain you have a level to check (or > else if what you said means “generics cannot be checked at all”, tell > why). I only say that they are not testable. Testing is necessary for large scale software design. Since you cannot separate generics from their instances, their usefulness for software decomposition is at least questionable. > Why should generic > usage be provable before instantiation ? Because you want to be able to deliver generic components. >> whatever does Ada with the instances of a generic body is irrelevant. > Why is its predictable behavior irrelevant? What is the behavior of a generic body? How would you define it? What are the specifications of generic body, not of a given instance? How to verify if the implementation is conformant to the specification? The strength of generics comes from patching the source code at a very low level. Deeper you descend less predictions could be made. -- Regards, Dmitry A. Kazakov http://www.dmitry-kazakov.de