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,2ff5c149712ec0eb X-Google-Attributes: gid103376,public,usenet X-Google-Language: ENGLISH,ASCII-7-bit Path: g2news1.google.com!news3.google.com!proxad.net!proxad.net!feeder2-2.proxad.net!newsfeed.arcor.de!newsspool2.arcor-online.net!news.arcor.de.POSTED!not-for-mail From: "Dmitry A. Kazakov" Subject: Re: Ada Interfaces and the Liskov Substitution Principle Newsgroups: comp.lang.ada User-Agent: 40tude_Dialog/2.0.15.1 MIME-Version: 1.0 Content-Type: text/plain; charset="us-ascii" Content-Transfer-Encoding: 7bit Reply-To: mailbox@dmitry-kazakov.de Organization: cbb software GmbH References: <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> <1180445634.5664.23.camel@kartoffel> <39viqigjwhrb$.gz67xvpinyjr.dlg@40tude.net> <465c9077$0$23135$9b4e6d93@newsspool1.arcor-online.net> Date: Wed, 30 May 2007 09:53:03 +0200 Message-ID: NNTP-Posting-Date: 30 May 2007 09:50:47 CEST NNTP-Posting-Host: 92193371.newsspool2.arcor-online.net X-Trace: DXC=OL30>nk_IXdOKO]LCQ@0g`A9EHlD;3Ycb4Fo<]lROoRa8kF=@MgA]j[6LHn;2LCVn7enW;^6ZC`dIXm65S@:3>oOcBcXnUE4Rc X-Complaints-To: usenet-abuse@arcor.de Xref: g2news1.google.com comp.lang.ada:15975 Date: 2007-05-30T09:50:47+02:00 List-Id: On Tue, 29 May 2007 22:46:12 +0200, Georg Bauhaus wrote: > Dmitry A. Kazakov wrote: >> This is all >> programming is about - porting mathematics. (:-)) To model the reality in >> just one hop might be just impossible for a normal programmer. You cannot >> rely on Nobel Price laureates, they are rare, expensive and uninterested in >> our problems. > > OK. So why should a normal programmer like me consider it a cost effective > idea to try to construct a proven mathematical model for my daily work? Why are you sure that your daily work isn't based on such models? You could use them unconsciously. >> How can you know that? (:-)) Let's take the braking control system for your >> next car... > > I hear that Mercedes engineers do not yet want to replace > the steering wheel with a embedded computer joy stick thing ... :-) > I think the argument is that a car must make quicker moves in more > constraining environments than your average airliner. Come on, embedded controllers operate the valves and ignition of the motor right now. Be sure burning is a lot faster than steering / braking. But that is not the point. The point one is - how would you enjoy the "spinal programming" model of things you do care? The second point is - why to program anything we don't care? >>> 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; >> >> Ordered set, mathematical induction etc. > > Uhm, can we have less than a group? Yes, as you don't mention the operation of. >>> and how does it help? >> >> A lot. For example it can tell the code reviewer that the above program is >> equivalent to: >> >> if k < 100 then >> k := 100; >> end if; > > Making assumptions about k ... This is how mathematics can make us prefer > default perspectives by moving all important points of view behind Formal > Mountains. The above change wouldn't have helped at all, on the contrary, > > for k'Address use ...; > > What's the mathematics of that, then? That k is a pair of functions mapping the system state to the value of k and reverse: Get_k : S -> Integer Set_k : S x Integer -> S Thank you for making my point! What mathematics makes here is all the rest, which could well be incomputable. Consider k a hardware random generator. You could not describe it in any programming language, but you can in the language of probability theory. -- Regards, Dmitry A. Kazakov http://www.dmitry-kazakov.de