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: a07f3367d7,39579ad87542da0e X-Google-Attributes: gida07f3367d7,public,usenet X-Google-NewGroupId: yes X-Google-Language: ENGLISH,UTF8 X-Received: by 10.68.112.65 with SMTP id io1mr5139108pbb.6.1368583591170; Tue, 14 May 2013 19:06:31 -0700 (PDT) Path: bp1ni2318pbd.1!nntp.google.com!npeer01.iad.highwinds-media.com!news.highwinds-media.com!feed-me.highwinds-media.com!border3.nntp.dca.giganews.com!border1.nntp.dca.giganews.com!border4.nntp.dca.giganews.com!border2.nntp.dca.giganews.com!nntp.giganews.com!newsfeed.news.ucla.edu!nrc-news.nrc.ca!News.Dal.Ca!citadel.nobulus.com!goblin3!goblin2!goblin.stu.neva.ru!aioe.org!.POSTED!not-for-mail From: =?utf-8?Q?Yannick_Duch=C3=AAne_=28Hibou57?= =?utf-8?Q?=29?= Newsgroups: comp.lang.ada Subject: Re: Seeking for papers about tagged types vs access to subprograms Date: Fri, 10 May 2013 13:18:12 +0200 Organization: Ada @ Home Message-ID: References: <17ceq51ydy3s0.s94miqqzbg5w.dlg@40tude.net> <1vrhb7oc4qbob$.q02vuouyovp5$.dlg@40tude.net> <19lrzzbgm77v6.1dzpgqckptaj6.dlg@40tude.net> <1bfhq7jo34xpi.p8n2vq6yjsea.dlg@40tude.net> <12gn9wvv1gwfk.10ikfju4rzmnj.dlg@40tude.net> NNTP-Posting-Host: uGUognJZXpdb++Da0QvCqg.user.speranza.aioe.org Mime-Version: 1.0 X-Complaints-To: abuse@aioe.org User-Agent: Opera Mail/12.15 (Linux) X-Notice: Filtered by postfilter v. 0.8.2 X-Received-Bytes: 5288 Content-Type: text/plain; charset=utf-8; format=flowed; delsp=yes Content-Transfer-Encoding: Quoted-Printable Date: 2013-05-10T13:18:12+02:00 List-Id: Le Fri, 10 May 2013 10:42:25 +0200, Dmitry A. Kazakov = a =C3=A9crit: > On Fri, 10 May 2013 05:29:53 +0200, Yannick Duch=C3=AAne (Hibou57) wro= te: > >> I tried to express each validity condition with types and then type = >> checking. > > You cannot express program semantics in terms of types. > > If you could express semantics, you won't need to program it. I don't understand what means =E2=80=9Cif you could express semantics, y= ou won't = need to program it=E2=80=9D. Or may be you meant the program is already = in the = described semantic? If so, that's indeed be true, as the program can the= n = be derived, but there is not a single possible derivation, there are = typically multiple solutions, so the program still requires human = intervention to be generated. Then if you see a types as set of axioms, and an instance of a type, as = = something with which the axioms are all turned into true hypothesis (you= = always need to prove hypothesis are true, before you can infer anything = = which in turn is true, and that must be at the object level for program)= , = then you express semantic with types. And types in Ada, already holds = axioms. Its axiom language is just too limited (ranges and available = operations, that's near to all what's available). Then again, semantic is expressed with axioms, or else that's not formal= = semantic, and that's, say, natural language semantic, always subject to = = possible subjective re=E2=80=91interpretation (no deterministic interpre= tation). I will be back to it later and I'm not versed in it enough so far, but = quickly, Isabelle/HOL (HOL stands for Higher Order Logic here), you have= = something close to that. With Isabelle, axioms and theorems may be = organized into classes or local theories, which are kind of generic whic= h = are to be instantiated, this instantiation being named =E2=80=9Can inter= pretation = of a local theory=E2=80=9D. You instantiate providing functions and valu= es as = arguments. With this kind of formal system, you typically go from a specification a= nd = derives a program. Ada do it the other way, and go from the program and = = prove it matches a specification later (either formally proving with SPA= RK = or using runtime=E2=80=91check), or immediately for what is statically c= hecked = (whether or not an operation exist, whether or not a value belongs to th= e = values of a type). But the concept does not imply a direction and would = = make as much sense with the Ada way to go from program and later prove o= r = check its properties: in both case, you have to express what is to be = verified, whatever you do it before you generate a program or after a = program was authored. If types could go beyond specification of a simple list of values (and w= e = already have a taste of that with discriminated records since always and= = invariant predicates since Ada 2012) and available sub=E2=80=93programs,= you won't = see types as you see it actually, it would look more expressive (and as = a = consequence, safer) and less =E2=80=9Crigid=E2=80=9D. -- = =E2=80=9CSyntactic sugar causes cancer of the semi-colons.=E2=80=9D [1] =E2=80=9CStructured Programming supports the law of the excluded muddle.= =E2=80=9D [1] [1]: Epigrams on Programming =E2=80=94 Alan J. =E2=80=94 P. Yale Univers= ity