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=ham autolearn_force=no version=3.4.4 X-Google-Thread: 103376,2ff5c149712ec0eb X-Google-Attributes: gid103376,public,usenet X-Google-Language: ENGLISH,ASCII-7-bit Path: g2news1.google.com!news3.google.com!news.germany.com!news.rh-tec.net!newsfeed.freenet.de!border2.nntp.ams.giganews.com!nntp.giganews.com!pe2.news.blueyonder.co.uk!blueyonder!feeder1-1.proxad.net!proxad.net!feeder2-2.proxad.net!newsfeed.arcor.de!newsspool2.arcor-online.net!news.arcor.de.POSTED!not-for-mail Newsgroups: comp.lang.ada Subject: Re: Ada Interfaces and the Liskov Substitution Principle From: Georg Bauhaus In-Reply-To: <1179953657.839272.160320@a26g2000pre.googlegroups.com> <1179991769.376381.252010@m36g2000hse.googlegroups.com> <12h6mi42jcha0.7f9vfsnihjwr$.dlg@40tude.net> <1180003336.1163.29.camel@kartoffel> <83abvs7sa9.fsf@hod.lan.m-e-leypold.de> <465aa5ba$0$23147$9b4e6d93@newsspool1.arcor-online.net> <465b6606$0$10188$9b4e6d93@newsspool4.arcor-online.net> Content-Type: text/plain Content-Transfer-Encoding: 7bit Message-Id: <1180445634.5664.23.camel@kartoffel> Mime-Version: 1.0 X-Mailer: Evolution 2.10.1 Date: Tue, 29 May 2007 15:33:54 +0200 Organization: Arcor NNTP-Posting-Date: 29 May 2007 15:33:54 CEST NNTP-Posting-Host: 15a09328.newsspool4.arcor-online.net X-Trace: DXC=dJh`QmUIGJTAX0F2i> On Tue, 2007-05-29 at 14:05 +0200, Dmitry A. Kazakov wrote: > > The idealized difference between programming oriented (model) research > > and researching formal properties of models is that, in the first case, > > you do not start from models only and then find different models, > > refine existing models etc.. You start in the programming shop, so to > > speak. > > But an application program is always a model of some physical reality. Yes. I just think that programs should be written with (a model of) physical reality in mind, but employ Off-the-Shelf standard models only if applicable. > > In fact, this is happening. For example, timing properties of > > co-operating procedures are captured in mathematical models. This is > > different from the ubiquitously alleged mathematicality of programming: > > that programs model mathematical functions. Some programs do, but is this > > all that matters? > > Yes, because application programming deals with mathematical models of the > reality. I doubt you could skip this abstraction layer. Programming deals with models of reality and, empirically, most of the time these models have properties that can be described using mathematics. Which is a good thing. However, asking for *mathematical* models of reality is asking for a clean room definition of the physical model in terms of mathematics. Many programs just happen to be a model of reality, and they still work well, even though they were not mathematically designed. The programmers are hardly aware of every conceivable mathematical property of their model. Still, they write sound programs. Can mathematics capture this process? Next, how much detail can you reasonably place in a formal specification of a model? Programming in UML seems to be over the top, IMHO, whereas modeling in UML using a reasonably small set of L isn't, of course. > > Shouldn't the relation between programs and mathematical > > functions be reversed? Wait, it is! > > You can consider mathematics or parts of as programming on some "axiomatic > hardware". What I want is the mathematics of program models, more than programming to satisfy mathematics. BTW, what is the best suited mathematical structure that (minimally) describes the loop while k < 100 loop k := Integer'succ(k); end loop; and how does it help?