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!out01a.usenetserver.com!news.usenetserver.com!in04.usenetserver.com!news.usenetserver.com!nx02.iad01.newshosting.com!newshosting.com!newsfeed2.ip.tiscali.net!tiscali!newsfeed1.ip.tiscali.net!feeder1-2.proxad.net!proxad.net!feeder2-2.proxad.net!newsfeed.arcor.de!newsspool1.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> <1180445634.5664.23.camel@kartoffel> <39viqigjwhrb$.gz67xvpinyjr.dlg@40tude.net> <465c9077$0$23135$9b4e6d93@newsspool1.arcor-online.net> <1180531107.16197.30.camel@kartoffel> Content-Type: text/plain Content-Transfer-Encoding: 7bit Message-Id: <1180611880.16197.59.camel@kartoffel> Mime-Version: 1.0 X-Mailer: Evolution 2.10.1 Date: Thu, 31 May 2007 13:44:40 +0200 Organization: Arcor NNTP-Posting-Date: 31 May 2007 13:44:35 CEST NNTP-Posting-Host: 059bf22d.newsspool1.arcor-online.net X-Trace: DXC=VS@^nTmE4:iJ00P1S40fZgic==]BZ:afn4Fo<]lROoRaFl8W>\BH3Yb;nL1onGoUSiN[W On Thu, 2007-05-31 at 12:27 +0200, Dmitry A. Kazakov wrote: > On Wed, 30 May 2007 15:18:27 +0200, Georg Bauhaus wrote: > > > I would start with a model that isn't originally inspired > > by mathematics (because higher math typically frowns upon operations, > > that is, the things that computers do). > > My vague model has loop invariants, loop termination, > > and the fact that the type Integer happens to include a successor > > function in its interface. Now, the type Integer offers much > > more than that, e.g. "*". Still, it seems reasonable to start from > > the mathematical structure that maps to a type like Integer, > > even when I do not need either of the inverse, > > the neutral element, or commutativity, which Integer types have > > (mostly), among other things. > > I don't see your point. You are saying that you don't need mathematics to > program, yet you illustrate your point using mathematical vocabulary. > There is something wrong with that. I'm saying that programmers do not necessarily write programs with mathematical structures in their head, but they still succeed. I don't call that unconscious mathematics, because we can't know that. It doesn't matter. When they write, a := a + 1; the may not be thinking about a commutative group of integers, and never use "-" or "0" in their program text. We may suggest, and many do (in particular in the non-Scheme FPL camp?), that program design should start from established pure mathematical structures only (or LSP, or ...). This way we will profit from the wealth of mathematical knowledge but we might also ignore successful solutions just because (1) they do not usually appear on math radar screens, or (2) contradict beliefs in known models (see co/contravariance). > >> Consider k a hardware random generator. > >> You could not describe it in any programming language, but you can in the > >> language of probability theory. > > > > Thank you for making my point! :-) Probability theoretic constructs > > can be mapped into executable computer constructs only in very limited > > ways, > No, the point is that they cannot be mapped (implemented), this is why > mathematics is necessary to describe what is going on, because no machine > would be sufficient for that. But what is actually going on in /dev/random?