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: a07f3367d7,39579ad87542da0e X-Google-Attributes: gida07f3367d7,public,usenet X-Google-NewGroupId: yes X-Google-Language: ENGLISH,UTF8 X-Received: by 10.180.109.166 with SMTP id ht6mr1644406wib.0.1368583636350; Tue, 14 May 2013 19:07:16 -0700 (PDT) Path: p18ni110084wiv.0!nntp.google.com!feeder1.cambriumusenet.nl!feed.tweaknews.nl!193.141.40.65.MISMATCH!npeer.de.kpn-eurorings.net!npeer-ng0.de.kpn-eurorings.net!border2.nntp.ams2.giganews.com!border4.nntp.ams.giganews.com!border2.nntp.ams.giganews.com!border2.nntp.dca.giganews.com!nntp.giganews.com!newsfeed.news.ucla.edu!nrc-news.nrc.ca!News.Dal.Ca!news.litech.org!news.stack.nl!aioe.org!.POSTED!not-for-mail From: "Dmitry A. Kazakov" Newsgroups: comp.lang.ada Subject: Re: Seeking for papers about tagged types vs access to subprograms Date: Fri, 10 May 2013 14:15:35 +0200 Organization: cbb software GmbH Message-ID: <1cir6d72wemw.qxx9mozot7hl.dlg@40tude.net> 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> Reply-To: mailbox@dmitry-kazakov.de NNTP-Posting-Host: 15waz9CoS+eMakbyhTPyFQ.user.speranza.aioe.org Mime-Version: 1.0 X-Complaints-To: abuse@aioe.org User-Agent: 40tude_Dialog/2.0.15.1 X-Notice: Filtered by postfilter v. 0.8.2 Content-Type: text/plain; charset="utf-8" Content-Transfer-Encoding: 8bit Date: 2013-05-10T14:15:35+02:00 List-Id: On Fri, 10 May 2013 13:18:12 +0200, Yannick Duchêne (Hibou57) wrote: > Le Fri, 10 May 2013 10:42:25 +0200, Dmitry A. Kazakov > a écrit: > >> On Fri, 10 May 2013 05:29:53 +0200, Yannick Duchêne (Hibou57) wrote: >> >>> 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 “if you could express semantics, you won't > need to program it”. Or may be you meant the program is already in the > described semantic? Program implements semantics. If you define the semantics using some other formalism you don't need the program anymore. The problem is that there is no formalism, or else the formalism is too powerful for being computable. > If so, that's indeed be true, as the program can then > 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. Human intervention is needed to handle the semantics, not because of multiplicity of implementations. You could choose them randomly. > 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). It is not axioms. However the axiomatic framework looks somewhat similar in the sense that rules of logical inference could be compared with the types algebra. But there is a sufficient difference that applying algebraic operations in programming is imperative. You never present a ready type in order to prove it being a result of some algebraic operations (=algebraic type). Maybe only in academic studies. Rather you apply operations directly and the result becomes algebraic merely per construction. > 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‑interpretation (no deterministic interpretation). No, the program semantics is the meaning of what the program does (to the customer). That lies outside the language. Not to confuse with the language semantics which describes how to execute the code (to the CPU). > 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 which > are to be instantiated, this instantiation being named “an interpretation > of a local theory”. You instantiate providing functions and values as > arguments. I am not familiar with that, but formal methods are always a meta language relatively to the programming language and its type system, which are the object language for them. You never mix the two. > With this kind of formal system, you typically go from a specification and > derives a program. That won't work. If you can derive the program (in the object language) you don't need the object language anymore. If that indeed works, as it does with the Assembly language, you move up to the meta language (higher-level programming language in this case) and forget about silly lower-level stuff. Regarding specification languages and modeling language I have serious reservations about them being capable to replace Ada and other general purpose languages. > If types could go beyond specification of a simple list of values (and we > already have a taste of that with discriminated records since always and > invariant predicates since Ada 2012) and available sub–programs, you won't > see types as you see it actually, it would look more expressive (and as a > consequence, safer) and less “rigid”. I don't see how Ada 2012 makes it more expressive. It did not extend types algebra in any significant way. BTW, static checks if have something to do with expressiveness, then by hampering it. Because it is evident that the more powerful constructs you have, less you could prove about their outcome. The most notorious example is goto. The art of language design is to deploy least powerful constructs, while keeping it useful for programming. -- Regards, Dmitry A. Kazakov http://www.dmitry-kazakov.de