From mboxrd@z Thu Jan 1 00:00:00 1970 Return-Path: X-Spam-Checker-Version: SpamAssassin 3.4.4 (2020-01-24) on inbox.vuxu.org X-Spam-Level: X-Spam-Status: No, score=-0.5 required=5.0 tests=DKIM_ADSP_CUSTOM_MED, DKIM_INVALID,DKIM_SIGNED,FREEMAIL_FORGED_FROMDOMAIN,FREEMAIL_FROM, HEADER_FROM_DIFFERENT_DOMAINS,MAILING_LIST_MULTI autolearn=ham autolearn_force=no version=3.4.4 Received: from minnie.tuhs.org (minnie.tuhs.org [50.116.15.146]) by inbox.vuxu.org (Postfix) with ESMTP id C42ED2236B for ; Sat, 25 May 2024 02:57:18 +0200 (CEST) Received: from minnie.tuhs.org (localhost [IPv6:::1]) by minnie.tuhs.org (Postfix) with ESMTP id 5835C43AC3; Sat, 25 May 2024 10:57:14 +1000 (AEST) Received: from mail-oo1-xc34.google.com (mail-oo1-xc34.google.com [IPv6:2607:f8b0:4864:20::c34]) by minnie.tuhs.org (Postfix) with ESMTPS id 303FF43AC0 for ; Sat, 25 May 2024 10:57:05 +1000 (AEST) Received: by mail-oo1-xc34.google.com with SMTP id 006d021491bc7-5b31f2c6e52so3485271eaf.2 for ; Fri, 24 May 2024 17:57:05 -0700 (PDT) DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/relaxed; d=gmail.com; s=20230601; t=1716598624; x=1717203424; darn=tuhs.org; h=in-reply-to:content-disposition:mime-version:references:message-id :subject:to:from:date:from:to:cc:subject:date:message-id:reply-to; bh=90AnfJqHzssDmb2VKcvrxt3RwO5/rC772GzF6EyenhU=; b=UeTJUdCfmq69QUliyPL0YdJdPQqnQLlkve2O3JfJTUnDG4nlhcQVmMzG6cNPnF4dxb E35rprWwNNyspirGO+e5O8S4ATASV7GLx8jSeC8EAW+wsHpWkYnw9P+fvkvbfS1am6UZ 56sFmmUVSk3YA4ZtEGKEFD1CLf5W1fgSRjWWXN3f0bFfD8lI450Mxca+b/epzSPqpllv HuLwhSR9dvq0SQ9nNEMg0FxNXPdmijj53aibHrTdO6jScjPB8bQ1ooYhuaA967Hydi5o 5cdb7xefbXZT1vmFn19LH+2T31CngKHOtkgwdZn6BAvGElVSD15Sg6cI8VCU7SNnqLxG st9A== X-Google-DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/relaxed; d=1e100.net; s=20230601; t=1716598624; x=1717203424; h=in-reply-to:content-disposition:mime-version:references:message-id :subject:to:from:date:x-gm-message-state:from:to:cc:subject:date :message-id:reply-to; bh=90AnfJqHzssDmb2VKcvrxt3RwO5/rC772GzF6EyenhU=; b=jcKtD8dpGSZSefJHUvRZhqCo/oK2r9bDGpoE1GoR9j124r1HjkODaEYrELQG/u3boD ovpZXw+Cn4fW4Vzdz/3OmROfTg6sG8UaZcxxfRUoIPDocU3x1+Sg/0mbbgkcMClUdMQR CE1gcVx1KCsCRGw3TIGADfS0b14IjKRDc4qMZQzQ5e76ywKzmxmRrxezOlTmycALxz2l V68eBA5dC5xZ8mY9nBT9BAqRPzR8njmJzXCmVNVSqsd9cN7TF0FEJ/LyOfAtnpmRevdY pLC9dBDhJqzltz1wrIgV3scZT5sQ4F8GYloXCoPuLocC12r8OHy0zI8e5jbCslO7o5X1 W6gg== X-Gm-Message-State: AOJu0Yz9khmOpE/SOflDY7Sc4OKq1CiWkHObjQgte0F8oMgWiECP4vLg 2phqtgplnHIzyjDnuU/DBMEdYBeVZAwnSKSxXEUbaScuuBikI48f4SOMNg== X-Google-Smtp-Source: AGHT+IFwae4Q1AJ4phJ56ocmkl75MduThDBd3chR/fGkTIxN5i68DLnzPmVxNjZI5YSwD8X7nQZAMQ== X-Received: by 2002:a05:6870:75cf:b0:244:c312:4c7c with SMTP id 586e51a60fabf-24ca11a31a0mr4794284fac.16.1716598623490; Fri, 24 May 2024 17:57:03 -0700 (PDT) Received: from illithid (ip68-12-97-90.ok.ok.cox.net. [68.12.97.90]) by smtp.gmail.com with ESMTPSA id 586e51a60fabf-24ca1ff63f2sm624529fac.15.2024.05.24.17.57.02 for (version=TLS1_3 cipher=TLS_AES_256_GCM_SHA384 bits=256/256); Fri, 24 May 2024 17:57:02 -0700 (PDT) Date: Fri, 24 May 2024 19:57:01 -0500 From: "G. Branden Robinson" To: The Unix Heritage Society mailing list Message-ID: <20240525005701.efxidwmww56qmiwa@illithid> References: <1E156D9B-C841-4693-BEA4-34C4BF42BCD5@iitbombay.org> MIME-Version: 1.0 Content-Type: multipart/signed; micalg=pgp-sha256; protocol="application/pgp-signature"; boundary="7vnzyow42s65xn5u" Content-Disposition: inline In-Reply-To: <1E156D9B-C841-4693-BEA4-34C4BF42BCD5@iitbombay.org> Message-ID-Hash: U67EEAG2VBFAECLGDD5MHKGN5HWB5275 X-Message-ID-Hash: U67EEAG2VBFAECLGDD5MHKGN5HWB5275 X-MailFrom: g.branden.robinson@gmail.com X-Mailman-Rule-Misses: dmarc-mitigation; no-senders; approved; emergency; loop; banned-address; member-moderation; nonmember-moderation; administrivia; implicit-dest; max-recipients; max-size; news-moderation; no-subject; digests; suspicious-header X-Mailman-Version: 3.3.6b1 Precedence: list Subject: [TUHS] Re: A fuzzy awk List-Id: The Unix Heritage Society mailing list Archived-At: List-Archive: List-Help: List-Owner: List-Post: List-Subscribe: List-Unsubscribe: --7vnzyow42s65xn5u Content-Type: text/plain; charset=us-ascii Content-Disposition: inline [restricting to list; strong opinions here] At 2024-05-24T17:17:53-0700, Bakul Shah via TUHS wrote: > What would be nice if programming languages provided some support for > such exhaustive testing[1]. [rearranging] > At one point I had suggested turning Go's Interface type to something > like Guttag style abstract data types in that relevant axioms are > specified right in the interface definition. It's an excellent idea. > The underlying idea is that each type is in essence a constraint on > what values an instance of that type can take. In the simple form of a data type plus a range constraint, that's the Ada definition of a subtype since day one--Ada '80 or Ada 83 if you insist on the standardized form of the language. 40 years later we have Linus Torvalds tearing up his achievement certificate in "kinder, gentler email interactions" just to trash the notion of range checks on data types.[1][2][3] Naturally, the brogrammers are quick to take Torvalds's side.[4] Pascal had range checks too, and Kernighan famously punked on Wirth for that. I'm not certain, but I get the feeling the latter got somewhat over-interpreted. (To be fair to Kernighan, Pascal _as specced in the Revised Report of 1973_[5] was in my opinion too weak a language to leave the lab, for many of the reasons he noted. The inflexible array typing was fatal, in my view.) > The idea was that any concrete type that implements that interface > must satisfy its axioms. Yes. There is of course much more to the universe of potential constraints than range checks. Ada 2022 has these in great generality with "subtype predicates". http://www.ada-auth.org/standards/22aarm/html/aa-3-2-4.html > Even if the compiler ignored these axioms, I don't understand why this idea wasn't seized upon with more force at the CSRC. The notion of a compiler flag that turned "extra" (in the Ritchie compiler circa 1980, this is perhaps expressed better as "any") correctness checks could not have been a novelty. NDEBUG and assert() are similarly extremely old even in Unix. > one can write a support program that can generate a set of > comprehensive tests based on these axioms. Yes. As I understand it, this is how Spark/Ada got started. Specially annotated comments expressing predicates communicated with such a support program, running much like the sort of automated theorem prover you characterize below as not "retail". In the last two revision cycles of the Ada standard (2013, 2022), Spark/Ada's enhancements have made it into the language--though I am not certain, and would not claim, that they compose with _every_ language feature. Spark/Ada started life as a subset of the language for a reason. But C has its own subset, MISRA C, so this is hardly a reason to scoff. > [Right now a type "implementing" an interface only needs to > have a set of methods that exactly match the interface methods but > nothing more] The underlying idea is that each type is in essence a > constraint on what values an instance of that type can take. So adding > such axioms simply tightens (& documents) these constraints. Just the > process of coming up with such axioms can improve the design (sor of > like test driven design but better!). Absolutely. Generally, software engineers like to operationalize things consistently enough that they can then be scripted/automated. Evidently software testing is so mind-numblingly tedious that the will to undertake it, even with automation, evaporates. > Now it may be that applying this to anything more complex than stacks > won't work well & it won't be perfect but I thought this was worth > experimenting with. This would be like functional testing of all the > nuts and bolts and components that go in an airplane. The airplane may > still fall apart but that would be a "composition" error! Yes. And even if you can prove 100% of the theorems in your system, you may learn to your dismay that your specification was defective. Automated provers are as yet no aid to system architects. > [1] There are "proof assisant" or formal spec languages such as TLA+, > Coq, Isabelle etc. but they don't get used much by the average > programmer. I want something more retail! I've had a little exposure to these. They are indeed esoteric, but also extremely resource-hungry. My _impression_, based on no hard data, is that increasing the abilities of static analyzers and the expressiveness with which they are directed with predicates is much cheaper. But a lot of programmers will not budge at any cost, and will moreover be celebrated by their peers for their obstinacy. See footnotes. There is much work still to be done. Regards, Branden [1] https://lore.kernel.org/all/202404291502.612E0A10@keescook/ https://lore.kernel.org/all/CAHk-=wi5YPwWA8f5RAf_Hi8iL0NhGJeL6MN6UFWwRMY8L6UDvQ@mail.gmail.com/ [2] https://lore.kernel.org/lkml/CAHk-=whkGHOmpM_1kNgzX1UDAs10+UuALcpeEWN29EE0m-my=w@mail.gmail.com/ [3] https://www.businessinsider.com/linus-torvalds-linux-time-away-empathy-2018-9 [4] https://lwn.net/Articles/973108/ [5] https://archive.org/details/1973-the-programming-language-pascal-revised-report-wirth --7vnzyow42s65xn5u Content-Type: application/pgp-signature; name="signature.asc" -----BEGIN PGP SIGNATURE----- iQIzBAABCAAdFiEEh3PWHWjjDgcrENwa0Z6cfXEmbc4FAmZRN1UACgkQ0Z6cfXEm bc6aLA//eGyuq1XcRZEPSM3ON8r8say08+r8QjnvJO6zJqw25PSot+H1Ca/8C0PE AndjtKClcGPb5S0A2URF8CAi1lNPdNC3OI5pZrpyJvocYDaYW06Gu37FWNF5aPex pdYBJHqBYnAzZMwm3U7ECg4wLvtBEUAubXZs+iyxBuiEZs/M56t4bqj4dobW5KHm iARdt0MbwrUu+4QOIkSV1QA5MN/RsqumCte6BpSoM9/HBhZa1Fl/jV3eHK4MAPFu +PZSXJ0FLg+MkLewdLQeh/O6s5OPNc2asndyzwfI4GF69el5V4U5mBgchTMo0WLW coFOxm+0s2513D+DmeOFHaleSQMZN584qGcKXVRKUWXBcv2DTtYKrfKZTp81ZEhh mXyPdYnpUW419pIIbxQx6rD1w75bx28OAR0CxZrmu+BRk4rEm2ccNknllkjnHRg/ TXwTa+VUCNJVInbjuG1nqrtBoPaZkHYhhlGaCbngu3ar8S7i98E2k5MQ9nurfry4 boI1jrFY59oAeYtDygguGzFBpLUIEJpoWNoXOOhcTyUW+KcO6kP0ZSERrGKyKg5C uanLBSx4yRZoeVGGdeJONuIj2px8SU7WoQCq5xl2G3nNO7hVQN93aiD3AFMswDy0 /l1nfRyAjmItJlc3VOfuPJmKYyAbpHgsTOjsN9rKcP3YxF5DjVQ= =h0I6 -----END PGP SIGNATURE----- --7vnzyow42s65xn5u--