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,29d8139471e3f53e X-Google-NewGroupId: yes X-Google-Attributes: gida07f3367d7,domainid0,public,usenet X-Google-Language: ENGLISH,ASCII-7-bit Path: g2news1.google.com!news3.google.com!feeder.news-service.com!kanaga.switch.ch!switch.ch!news.belwue.de!newsfeed.arcor.de!newsspool3.arcor-online.net!news.arcor.de.POSTED!not-for-mail Date: Tue, 14 Sep 2010 23:18:36 +0200 From: Georg Bauhaus User-Agent: Mozilla/5.0 (Macintosh; U; Intel Mac OS X 10.6; en-US; rv:1.9.2.9) Gecko/20100825 Thunderbird/3.1.3 MIME-Version: 1.0 Newsgroups: comp.lang.ada Subject: Re: Securing type extensions References: <87iq2bfenl.fsf@mid.deneb.enyo.de> <874odv9npv.fsf@ludovic-brenta.org> <87y6b7cedd.fsf@mid.deneb.enyo.de> <66a3704c-54f9-4f04-8860-aa12f516134b@t3g2000vbb.googlegroups.com> <87d3sib44t.fsf@mid.deneb.enyo.de> <134q4k2ly2pf4$.17nlv1q6q5ivo.dlg@40tude.net> <4c8dec8e$0$6990$9b4e6d93@newsspool4.arcor-online.net> <4c8e3f44$0$6769$9b4e6d93@newsspool3.arcor-online.net> <4c8e87f8$0$6877$9b4e6d93@newsspool2.arcor-online.net> <4c8f4833$0$6763$9b4e6d93@newsspool3.arcor-online.net> <2ka8sfdvyvil.1k714obgzgj3a.dlg@40tude.net> In-Reply-To: <2ka8sfdvyvil.1k714obgzgj3a.dlg@40tude.net> Content-Type: text/plain; charset=ISO-8859-1; format=flowed Content-Transfer-Encoding: 7bit Message-ID: <4c8fe6ad$0$6759$9b4e6d93@newsspool3.arcor-online.net> Organization: Arcor NNTP-Posting-Date: 14 Sep 2010 23:18:37 CEST NNTP-Posting-Host: 188746be.newsspool3.arcor-online.net X-Trace: DXC=C>Q^AC=ZH?LI7\_^6>c20JMcF=Q^Z^V3H4Fo<]lROoRA8kFejVHkh`15BShUBC^9]D@_XDICF X-Complaints-To: usenet-abuse@arcor.de Xref: g2news1.google.com comp.lang.ada:14083 Date: 2010-09-14T23:18:37+02:00 List-Id: On 9/14/10 2:22 PM, Dmitry A. Kazakov wrote: > On Tue, 14 Sep 2010 12:02:28 +0200, Georg Bauhaus wrote: > >> I'm asking about visibility and how it can possibly help ascertaining >> that user supplied subprograms are trustworthy---which is, by >> definition, not the same thing as "safe". > > Hmm, how "trustworthiness" corresponds to correctness and type safety? I'd consider the relation of trustworthiness, correctness and type safety at least from two viewpoints, a technical one and one on conflict: 1 - Technically, a program may have certain formal properties, such as no type errors. (Like a program can suffer if written in Python). Each formal property may exclude precisely the corresponding class of errors, if there is such correspondence. Suppose a partial program has "sockets" into which foreign code can be plugged, to make it complete. Such as a type extension with overridden subprograms. The completion is done on site. At the very least the interfaces must match. But the parent type's "plan" might require that the type's operations be called in a certain order, sayoperation A is called before operation D, no matter what comes in between. An exception is thrown otherwise, or worse. So both, the programmer who has written the partial program and the programmer who has written the plug-in code may have an interest in following the plan. How do you talk about this on site? Can you trust the plug-in code? Suppose you don't use Ada, but Python or some other more dynamically typed language. Can you even assume the type has the same interface as its parent? When the absence of a statically known interface destroys all hope for type safety, how can programmers sill trust Google to continue providing meaningful Python objects for Google App Engine? 2 - The utility function of a business might include a variable that stands for cost of conflict. Cost of conflict is in part negotiated, in part a consequence of the legal system. The conflict here is triggered by a malfunctioning program: who/what is to blame when a type extension (by party X) does not work nicely with a partial program (by party Y)? Demonstrable correctness and type safety can be turned into arguments. "Clearly, our partial program is correct, and type safe. Therefore, your type extension makes the product malfunction." -- "But we only varied the order of calls and your type specifies nothing in this area. Why didn't you specify ordering requirements as preconditions?" ... So do correctness and type safety make two parties trust each other with their business? In a more peaceful setting, the utility function of a business might include a variable that stands for income that only high quality software can generate. (Assuming that customers will pay a higher price for a better product.) Again, demonstrable correctness and type safety can be turned into arguments. If correctness and type safety contribute to high quality, if high quality entails a higher price, and if paying a higher price expresses trustworthiness, then correctness and type safety yield trust. (There are other reasons for larger sums payed, but I'll ignore them.) Georg