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,HTML_MESSAGE,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 DF55B26898 for ; Sat, 25 May 2024 19:18:35 +0200 (CEST) Received: from minnie.tuhs.org (localhost [IPv6:::1]) by minnie.tuhs.org (Postfix) with ESMTP id C5CC343B2E; Sun, 26 May 2024 03:18:31 +1000 (AEST) Received: from mail-pj1-x1033.google.com (mail-pj1-x1033.google.com [IPv6:2607:f8b0:4864:20::1033]) by minnie.tuhs.org (Postfix) with ESMTPS id 56EDC43B2D for ; Sun, 26 May 2024 03:18:27 +1000 (AEST) Received: by mail-pj1-x1033.google.com with SMTP id 98e67ed59e1d1-2bf7fec9926so835188a91.2 for ; Sat, 25 May 2024 10:18:27 -0700 (PDT) DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/relaxed; d=gmail.com; s=20230601; t=1716657506; x=1717262306; darn=tuhs.org; h=to:subject:message-id:date:from:in-reply-to:references:mime-version :from:to:cc:subject:date:message-id:reply-to; bh=4Sb/P4pl6ZF8/+E146X7+q8kBn4g6ihwlxqiEJLBXss=; b=j4sC/liOp9fF5xtBo2H/MouRieoYXpCxrEuG4mG8PKINxeM5RjkckN6bkaxAhii2X9 COvzDNkBsiVaj/W0XWjuxOUFqwNz98TOs/HAKp+vIr+tnTHP1IhZS6I7iz9FJgeAZYXy IzgPMkG26qzSWOtcfjtkElxWBHe4DeaO+VtO2DpN5KbFyqQ/pi50jVmF2sDSJg8o5fKx hKXSmJRGWwmfMyZIv6oinIJfCRVzQXzv/9kb+LCjPArNnsRnGwdO0KJA028+gRZi7EiR G1acdYlBjb1T+EaxkEZGHxs7FPY2oVgyRGRWT+5RoNTyAMAdZA/Uu2Bu6xnsHeIZ1KKt 8Itg== X-Google-DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/relaxed; d=1e100.net; s=20230601; t=1716657506; x=1717262306; h=to:subject:message-id:date:from:in-reply-to:references:mime-version :x-gm-message-state:from:to:cc:subject:date:message-id:reply-to; bh=4Sb/P4pl6ZF8/+E146X7+q8kBn4g6ihwlxqiEJLBXss=; b=mqFFi3Y5vkPDjbJ6/UsNn8eSCX/2GK/YQ9d8wwo/y9WCcmf/tiqkWCe6nnenmi4rZg e2y6aEM+Lv1ZEfwejBxsHHWUKr/z5x09crYgwS31CpmVDjVG3roBi2GV7X4NmCBIJojx UXHliaBRClGQGQLYCKsjhQQ0Zj0CrSl+EYA6l2sYEZ3UB9foBdOUSo7oxJ9Y6gwcWTNt gI9uNyFdMaHYfGUCnckaSf3K002kUEkLRsh7ljmeJc+oeDkTQT4kiarQbVPha0wAOKvJ CY5nLtgySpuOb/fdNXNG6ROxuYb7OwejdGgoGgTBucOFUayQgUJXrenybCbI+EMHwOQe PQ1A== X-Gm-Message-State: AOJu0YwB3ZjY1W9W+bSpm0xl7aGQrRNfAZrxWoLlCpTPMLnTOM+oAmpi zp5dvXGxxj6OYovOZhC4J1O4ZzcfDf3qOgSZgEPryS69e9lWjeyXFtwunmtNPQGrV0mcrEMRS9J mgpJS9e+dXEx9PjEZ4N/0hw8mRqmz9w== X-Google-Smtp-Source: AGHT+IHj8tK8w34wyIUpWnvKxozCktspk6A7wQHhkYS6jSxty7GZUXqBt3/5H64d9r3MwGsjEy3FakAJHqECTVIpRXY= X-Received: by 2002:a17:90b:684:b0:2bd:d488:9336 with SMTP id 98e67ed59e1d1-2bf5ef1bb89mr4682091a91.24.1716657506344; Sat, 25 May 2024 10:18:26 -0700 (PDT) MIME-Version: 1.0 References: <1E156D9B-C841-4693-BEA4-34C4BF42BCD5@iitbombay.org> In-Reply-To: <1E156D9B-C841-4693-BEA4-34C4BF42BCD5@iitbombay.org> From: Paul Winalski Date: Sat, 25 May 2024 13:18:17 -0400 Message-ID: To: The Unix Heritage Society mailing list Content-Type: multipart/alternative; boundary="000000000000ddee4e06194a78bc" Message-ID-Hash: K7KF4LX6ADP6ZQZJBP3GZAAAFMD3OIHQ X-Message-ID-Hash: K7KF4LX6ADP6ZQZJBP3GZAAAFMD3OIHQ X-MailFrom: paul.winalski@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: --000000000000ddee4e06194a78bc Content-Type: text/plain; charset="UTF-8" Content-Transfer-Encoding: quoted-printable On Fri, May 24, 2024 at 8:18=E2=80=AFPM Bakul Shah via TUHS = wrote: 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. The idea was that any concrete type th= at > implements that interface must satisfy its axioms. Even if the compiler > ignored these axioms, one can write a support program that can generate a > set of comprehensive tests based on these axioms. [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 o= f > 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!). > At one point I worked with a programming language called Gypsy that implemented this concept. Each routine had a prefix that specified axioms on the routine's parameters and outputs. The rest of Gypsy was a conventional procedural language but the semantics were carefully chosen to allow for automated proof of correctness. I wrote a formal specification for the DECnet session layer protocol (DECnet's equivalent of TCP) in Gypsy. I turned up a subtle bug in the prose version of the protocol specification in the process. -Paul W. --000000000000ddee4e06194a78bc Content-Type: text/html; charset="UTF-8" Content-Transfer-Encoding: quoted-printable
On Fri, May 24, 2024 at 8:18=E2=80=AFPM B= akul Shah via TUHS <tuhs@tuhs.org&g= t; wrote:

At one point I had su= ggested turning Go's Interface type to something like Guttag style abst= ract data types in that relevant axioms are specified right in the interfac= e definition. The idea was that any concrete type that implements that inte= rface must satisfy its axioms. Even if the compiler ignored these axioms, o= ne can write a support program that can generate a set of comprehensive tes= ts based on these axioms. [Right now a type "implementing" an int= erface 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 esse= nce a constraint on what values an instance of that type can take. So addin= g 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!).

At one point I worked with a programming language called Gypsy that imple= mented this concept.=C2=A0 Each routine had a prefix that specified axioms = on the routine's parameters and outputs.=C2=A0 The rest of Gypsy was a = conventional procedural language but the semantics were carefully chosen to= allow for automated proof of correctness.=C2=A0 I wrote a formal specifica= tion for the DECnet session layer protocol (DECnet's equivalent of TCP)= in Gypsy.=C2=A0 I turned up a subtle bug in the prose version of the proto= col specification in the process.

-Paul W.
--000000000000ddee4e06194a78bc--