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 8897A23C14 for ; Sat, 25 May 2024 19:37:14 +0200 (CEST) Received: from minnie.tuhs.org (localhost [IPv6:::1]) by minnie.tuhs.org (Postfix) with ESMTP id DBC9943B3D; Sun, 26 May 2024 03:37:10 +1000 (AEST) Received: from mail-lj1-x233.google.com (mail-lj1-x233.google.com [IPv6:2a00:1450:4864:20::233]) by minnie.tuhs.org (Postfix) with ESMTPS id 5C88D43B3C for ; Sun, 26 May 2024 03:37:07 +1000 (AEST) Received: by mail-lj1-x233.google.com with SMTP id 38308e7fff4ca-2e95abc7259so18962351fa.3 for ; Sat, 25 May 2024 10:37:07 -0700 (PDT) DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/relaxed; d=gmail.com; s=20230601; t=1716658625; x=1717263425; darn=tuhs.org; h=cc:to:subject:message-id:date:from:in-reply-to:references :mime-version:from:to:cc:subject:date:message-id:reply-to; bh=XaE1pddc+COL2m2Necb88yTmPk+hUARqbyFUS7Bdp18=; b=grnLgxHDu0uuyKTJuDedJScpzmPppPS2NSBKR5apshbuIPOTagU911RZjMnuRZScWS pZazRXmKq5FrQr4W4D2qV56fspL2Os2scrx0OOsuwFtCMWaO70seilIIEwSpq8to6V/C Ijt9P81uVrM5Lw+aqxaalipQ6Tndi2dXX5UpxKlNGgLucqgVKSxhaLjv27GpjbQqMmVF eD2rrZomsJ00dV4l4l6CrGY4Hud3RENNqyzBgiiYtwvAg8+o3o6K1gQKxPEc2t9fkDWh EeYE5Xg4cbLckCNchxDu7kkWSiZnnZ8ApeXV+3MR50aVRxLJ9bjMv4AMzSnmNXbehqIi Rv1w== X-Google-DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/relaxed; d=1e100.net; s=20230601; t=1716658625; x=1717263425; h=cc: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=XaE1pddc+COL2m2Necb88yTmPk+hUARqbyFUS7Bdp18=; b=klbYCLtnTOzLWP2VSFTlb7HbDU449chocqmOgPugTxNmQCzki6zFGNqGsM+2jGrYT2 komcDpetD/xQcAqtDlQJMQR3CXnPLkRfSRhisG/cyxOfm4UfWwEGjIhpu/qsQfKyaQWy jlCUZhGqEuJrpwpuMEe5HO0J8tXUHtjrL1MNUDEEYJ+iIvwAV+s951yxHaR32dRy2YbM 3u4TKJ0HG8fP0LxYsbDynUR1UUXKSzyglCqvnMCv6M4y8/sH4sKirfJ/8uEXzBE/Dzax E7eBRIhZW77cPCRbQkYew2JGqnorgHyr8VGZosGSaCJiTNvB5Kl/j248Ngxhpwzu+vZz 6mCQ== X-Gm-Message-State: AOJu0YyInWGKClZ/dWfj694NzeMbvKcQjl+RAz9NlDuFHAGJ4YyuTPsB YzmHtAcVuLGNRIowrHrXLag2WTNdpvAxDEEFASzJLlVEV5T9ANxp8KPA40w/QEvfhAdKCANMXS4 spR5iRES26xFyJLUIXgXPpMQdgze7UA== X-Google-Smtp-Source: AGHT+IH0AZq1UTNpMiUg3vA0BOwDQcvQZH3EEK+MSKEcH/h7Yc/UhpXNwfxS2zLis4NyinqmOmkcNsHyd6t4WSzN1ZI= X-Received: by 2002:a19:5e09:0:b0:51f:2709:3641 with SMTP id 2adb3069b0e04-529645e4f17mr2813817e87.26.1716658625153; Sat, 25 May 2024 10:37:05 -0700 (PDT) MIME-Version: 1.0 References: <1E156D9B-C841-4693-BEA4-34C4BF42BCD5@iitbombay.org> In-Reply-To: From: Tom Perrine Date: Sat, 25 May 2024 10:36:53 -0700 Message-ID: To: Paul Winalski Content-Type: multipart/alternative; boundary="0000000000008d93b206194abb91" Message-ID-Hash: XJCQIVH7UXFI344INOXB7ZDJKTWA52TG X-Message-ID-Hash: XJCQIVH7UXFI344INOXB7ZDJKTWA52TG X-MailFrom: tom.perrine@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 CC: The Unix Heritage Society mailing list 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: --0000000000008d93b206194abb91 Content-Type: text/plain; charset="UTF-8" Content-Transfer-Encoding: quoted-printable Another Gypsy user here... For KSOS-11 the kernel was described in SPECIAL - as a set of axioms and theorems. There was no actual connection between the formal specification in SPECIAL and the Modula code. Some of the critical user-space code for a trusted downgrade program, to bridge data from higher levels of classification to lower, was written in Gypsy. I visited UT Austin and Dr Good(?)'s team to learn it, IIRC. Gypsy was considered better in that the specification was tied to the executable through the pre/post conditions - and the better support for semi-automated theorem proving. On Sat, May 25, 2024 at 10:18=E2=80=AFAM Paul Winalski wrote: > 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 lik= e >> Guttag style abstract data types in that relevant axioms are specified >> right in the interface definition. The idea was that any concrete type t= hat >> 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 ide= a >> 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!). >> > > At one point I worked with a programming language called Gypsy that > implemented this concept. Each routine had a prefix that specified axiom= s > 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. > --0000000000008d93b206194abb91 Content-Type: text/html; charset="UTF-8" Content-Transfer-Encoding: quoted-printable
Another Gypsy user here...

For KSOS-11 = the kernel was described in SPECIAL - as a set of axioms and theorems. Ther= e was no actual connection between the formal specification in SPECIAL and = the Modula code.

Some of the critical user-space c= ode for a trusted downgrade program, to bridge data from higher levels of c= lassification to lower, was written in Gypsy. I visited UT Austin and Dr Go= od(?)'s team to learn it, IIRC. Gypsy was considered better in that the= specification was tied to the executable through the pre/post conditions -= and the better support for semi-automated theorem=C2=A0proving.
=



On Sat, May 25, 2024 at 10:18=E2=80= =AFAM Paul Winalski <paul.win= alski@gmail.com> wrote:
On Fri, May 24, 2024 at 8:= 18=E2=80=AFPM Bakul Shah via TUHS <tuhs@tuhs.org> wrote:

=