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,FREEMAIL_FROM autolearn=ham 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!news4.google.com!feeder.news-service.com!94.75.214.39.MISMATCH!aioe.org!not-for-mail From: =?utf-8?Q?Yannick_Duch=C3=AAne_=28Hibou57?= =?utf-8?Q?=29?= Newsgroups: comp.lang.ada Subject: Re: Do people who use Ada also use ocaml or F#? Date: Sat, 30 Oct 2010 22:04:34 +0200 Organization: Ada @ Home Message-ID: References: <87k4kz3mda.fsf@mid.deneb.enyo.de> <5jjgrklivesk$.z0is5qe7mgbt.dlg@40tude.net> NNTP-Posting-Host: gHYtk+mhCrTAX6LNXybaBQ.user.speranza.aioe.org Mime-Version: 1.0 Content-Type: text/plain; charset=utf-8; format=flowed; delsp=yes Content-Transfer-Encoding: Quoted-Printable X-Complaints-To: abuse@aioe.org X-Notice: Filtered by postfilter v. 0.8.2 User-Agent: Opera Mail/10.63 (Win32) Xref: g2news2.google.com comp.lang.ada:15958 Date: 2010-10-30T22:04:34+02:00 List-Id: Le Sat, 30 Oct 2010 21:37:31 +0200, Dmitry A. Kazakov = a =C3=A9crit: >> 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 argume= nt = > 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. What is different than when you re-use a method from= a = library and that library was not specifically designed for your = application ? You have to check what you re-use is indeed the (or one of= ) = the good stuff to use. > So are machine instructions when executed by the processor. Everything is better checked at multiple level of precisions : at the = requirement/expectation level, at the model level, at the implementation= = design level, at the binary produced by the compiler. Real safety requir= es = check up to the level of machine code (and CPU and so on), less safety = requires less check (unless a big-bug occurs and you suspect the compile= r). If I understand you correctly, you complain you have a level to check (o= r = else if what you said means =E2=80=9Cgenerics cannot be checked at all=E2= =80=9D, tell = why). That is what is strange to me. Not provable, is one thing, provabl= e = at this stage instead of this one is another topic. Why should generic = usage be provable before instantiation ? (you have at least a proof of = some consistency with Ada, even before instantiation). > whatever does Ada with the instances of a generic body is irrelevant. Why is its predictable behavior irrelevant ? Isn't it the opposite ? -- = Si les chats miaulent et font autant de vocalises bizarres, c=E2=80=99es= t pas pour = les chiens.