Re: [Edm] Tracking (and distinguishing) formal analysis

Lucas Pardue <lucaspardue.24.7@gmail.com> Wed, 15 March 2023 14:14 UTC

Return-Path: <lucaspardue.24.7@gmail.com>
X-Original-To: edm@ietfa.amsl.com
Delivered-To: edm@ietfa.amsl.com
Received: from localhost (localhost [127.0.0.1]) by ietfa.amsl.com (Postfix) with ESMTP id E6DDDC1522D7 for <edm@ietfa.amsl.com>; Wed, 15 Mar 2023 07:14:16 -0700 (PDT)
X-Virus-Scanned: amavisd-new at amsl.com
X-Spam-Flag: NO
X-Spam-Score: -1.847
X-Spam-Level:
X-Spam-Status: No, score=-1.847 tagged_above=-999 required=5 tests=[BAYES_00=-1.9, DKIM_SIGNED=0.1, DKIM_VALID=-0.1, DKIM_VALID_AU=-0.1, DKIM_VALID_EF=-0.1, FREEMAIL_ENVFROM_END_DIGIT=0.25, FREEMAIL_FROM=0.001, HTML_MESSAGE=0.001, RCVD_IN_DNSWL_NONE=-0.0001, RCVD_IN_ZEN_BLOCKED_OPENDNS=0.001, SPF_HELO_NONE=0.001, SPF_PASS=-0.001] autolearn=ham autolearn_force=no
Authentication-Results: ietfa.amsl.com (amavisd-new); dkim=pass (2048-bit key) header.d=gmail.com
Received: from mail.ietf.org ([50.223.129.194]) by localhost (ietfa.amsl.com [127.0.0.1]) (amavisd-new, port 10024) with ESMTP id lfejvt8LdOTL for <edm@ietfa.amsl.com>; Wed, 15 Mar 2023 07:14:16 -0700 (PDT)
Received: from mail-oa1-x2f.google.com (mail-oa1-x2f.google.com [IPv6:2001:4860:4864:20::2f]) (using TLSv1.3 with cipher TLS_AES_128_GCM_SHA256 (128/128 bits) key-exchange X25519 server-signature RSA-PSS (2048 bits) server-digest SHA256) (No client certificate requested) by ietfa.amsl.com (Postfix) with ESMTPS id 7F9CDC15154D for <edm@iab.org>; Wed, 15 Mar 2023 07:14:16 -0700 (PDT)
Received: by mail-oa1-x2f.google.com with SMTP id 586e51a60fabf-177b78067ffso9981186fac.7 for <edm@iab.org>; Wed, 15 Mar 2023 07:14:16 -0700 (PDT)
DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/relaxed; d=gmail.com; s=20210112; t=1678889655; h=cc:to:subject:message-id:date:from:in-reply-to:references :mime-version:from:to:cc:subject:date:message-id:reply-to; bh=Gz97vW5nM7Ns7q4Itpxj7tiv58F8xW7ghBsADq+K2jU=; b=ev7ezZoumJtumccSzEyQxmdSqGr482GNv6IEPh2lP3oZAdhtqZ7R+GOsA1X8JcDG1W x24GKW6a+LIOORLc3qwG72lzIBEdu/RhaqyBiLxZqb4Fr8Mj5LqvITkh/YuAdwEB7xHX veOB5fmvrVNoti/2y98/QXvWJMlZFFVE7wN+EL6pHQtt8kFM7SpAG3HY5VLS4B3PXTJr qMRWa1ut4ioqeMx9kuojYMsh2/eSsS/CK8N4IgCkKFFAqn6JEUpAzgB/wbyqhELwMObv qpmc0xrMfecalKjm5Srqt7hf7FbNIE+lHnB/FCzLxSBHfcJIXwYbUyUyb1dAElePlNbQ TsNw==
X-Google-DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/relaxed; d=1e100.net; s=20210112; t=1678889655; 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=Gz97vW5nM7Ns7q4Itpxj7tiv58F8xW7ghBsADq+K2jU=; b=en0Ve8ZfuAbOmEoqwStEs1TtHOZhtYvGl09FyAS5aSRU2+CxeGJHV5JRTd1Qe+LOSc uilRsjDZulZwKp2mGToBs1qPv/t/v2zGGDLOvFcfPRXHYkrBXiW6/G7fShA2v6IG83LM qPJxCM3fx5/++Ga3fx6fyphjeCb4fEibmPOOH2HiWH9C6XB6C9YoVktnv3dQ1n4JW0Cp WWUovcSqX+OsCYYLSyNWdIqbZG4CLrNFckoVJq37p/Jqh9ZhyHXy+v5+8kDwXNqQk2WE e0Q9OegUoJbfKbSSGcjx4eHqRWW70TUQ8A4z9gxUM4N6RKHiTlMc9aMc0mqeI8QP5Jjg JOgA==
X-Gm-Message-State: AO0yUKXITamq7GzsewmHVrokfyBLrVlS3F15F+U6R6mEeEL9RNR6vfeA /RlJWOfpaLQUPcFjw2cLl21oh11HykJ4kC+c9dM=
X-Google-Smtp-Source: AK7set8lwaKef3PE4TpLJfUhET550s7j8JQoJau1bc/Mu7ZHdj4ki+pboF4IJflSkcCwg87MIJ5AVLA77Q0Q/q4JgjA=
X-Received: by 2002:a05:6870:9e87:b0:17a:b31c:9e1b with SMTP id pu7-20020a0568709e8700b0017ab31c9e1bmr2490420oab.3.1678889655212; Wed, 15 Mar 2023 07:14:15 -0700 (PDT)
MIME-Version: 1.0
References: <CALGR9obBioR7UFjWB-sGA96DBsMXBu7LNByDk-XRfM9DayeVSQ@mail.gmail.com> <D2AD3E3F-77F8-4F8B-A4F3-92386E58E997@heapingbits.net>
In-Reply-To: <D2AD3E3F-77F8-4F8B-A4F3-92386E58E997@heapingbits.net>
From: Lucas Pardue <lucaspardue.24.7@gmail.com>
Date: Wed, 15 Mar 2023 14:14:01 +0000
Message-ID: <CALGR9oYbWTUDMLR53kgyM+8N94hic16nQrj0vV=uuq+DVCTmwQ@mail.gmail.com>
To: Christopher Wood <caw@heapingbits.net>
Cc: edm@iab.org
Content-Type: multipart/alternative; boundary="0000000000008420a705f6f0f599"
Archived-At: <https://mailarchive.ietf.org/arch/msg/edm/s1zOJs844Tmy5EiLX1ZOvfy1oj0>
Subject: Re: [Edm] Tracking (and distinguishing) formal analysis
X-BeenThere: edm@iab.org
X-Mailman-Version: 2.1.39
Precedence: list
List-Id: "Evolvability, Deployability, & Maintainability \(Proposed\) Program" <edm.iab.org>
List-Unsubscribe: <https://www.iab.org/mailman/options/edm>, <mailto:edm-request@iab.org?subject=unsubscribe>
List-Archive: <https://mailarchive.ietf.org/arch/browse/edm/>
List-Post: <mailto:edm@iab.org>
List-Help: <mailto:edm-request@iab.org?subject=help>
List-Subscribe: <https://www.iab.org/mailman/listinfo/edm>, <mailto:edm-request@iab.org?subject=subscribe>
X-List-Received-Date: Wed, 15 Mar 2023 14:14:17 -0000

On Wed, 15 Mar 2023, 14:02 Christopher Wood, <caw@heapingbits.net> wrote:

> I agree that it’s useful for drafts to cite this work, but we should also
> acknowledge that analyses change over time. Sometimes there are bugs in the
> proofs or models. Sometimes new results emerge that complement or otherwise
> impact existing analyses. The unfortunate consequence of immutable RFCs is
> that we don’t have a good way to track these things. Adding them to the
> datatracker seems like a low effort workaround.
>

Apologies if I was unclear, I totally agree that using the datatrackef as
you suggest is good. Cataloging other work publicly has an upshot of making
it more visible, so RFC updates or related new documents might then pick
something to more formally cite.

It's not hard to add to the datatracker, but distributing/minimising the
effort to update the list might encourage more use.

Cheers
Lucas