Internet-Draft | Computerate Specification | August 2024 |
Petit-Huguenin | Expires 6 February 2025 | [Page] |
This document specifies computerate specifications, which are the combination of a formal and an informal specification such as parts of the informal specification are generated from the formal specification.¶
This Internet-Draft is submitted in full conformance with the provisions of BCP 78 and BCP 79.¶
Internet-Drafts are working documents of the Internet Engineering Task Force (IETF). Note that other groups may also distribute working documents as Internet-Drafts. The list of current Internet-Drafts is at https://datatracker.ietf.org/drafts/current/.¶
Internet-Drafts are draft documents valid for a maximum of six months and may be updated, replaced, or obsoleted by other documents at any time. It is inappropriate to use Internet-Drafts as reference material or to cite them other than as "work in progress."¶
This Internet-Draft will expire on 6 February 2025.¶
Copyright (c) 2024 IETF Trust and the persons identified as the document authors. All rights reserved.¶
This document is subject to BCP 78 and the IETF Trust's Legal Provisions Relating to IETF Documents (https://trustee.ietf.org/license-info) in effect on the date of publication of this document. Please review these documents carefully, as they describe your rights and restrictions with respect to this document. Code Components extracted from this document must include Revised BSD License text as described in Section 4.e of the Trust Legal Provisions and are provided without warranty as described in the Revised BSD License.¶
An informal specification is any document that is the combination of text, diagrams, tables, lists, and examples and whose purpose is to describe an engineering system. An RFC is an example of informal specification when it describes network elements and the protocols that help these elements to interoperate.¶
Informal specifications are nowadays written on a computer, which makes them easier to write but not easier to reason about their correctness. Computers can be used to model the engineering system that a specification is meant to describe, to verify that some properties hold for that model, and to automatically derive parts of the text, diagrams, list and examples that compose that specification. This could be done in an ad-hoc way by copying and pasting results from external software, but this adds the burden for the specification authors of having to keep the software model and the specification synchronized.¶
A well-known consequence is when an example in a specification does not match the text, most likely because one of the two was modified without verifying that the other was updated.¶
To simplify the integration of code in a specification we introduce the concept of "Computerate Specifying", which is similar in appearance to literate programming [LitProg], but reversing the intent. Literate programming is about interspersing code with the elements of a document, with the intent of producing a piece of code that can then be executed. On the other hand computerate specifying is about interspersing a document with code, with the intent of producing a document that have some of its elements generated from the result of computations that uses that code.¶
"Computerate Specifying" is a play on "Literate Computing", itself a play on "Structured Computing" (see [Knuth92] page 99). Note that "computerate" is a British English word. To keep on the joke, an informal specification could be said to be an incomputerate specification, "incomputerate" being an Australian English word.¶
There is a large variety of target formats in which a specification can be written (HTML, PDF, Word, Confluence), so we use [AsciiDoc] as a common format from which any of the target formats can be generated.¶
AsciiDoc is a text format, making it easy to mix with code and to integrate with the tools that programmers are most familiar with. It has been chosen because it is derived from DocBook and because its main implementation, [Asciidoctor], can be easily extended and already have a large set of backends for various target formats:¶
The AsciiDoc syntax is enriched with several extensions designed to support computerate specifications:¶
These syntax extensions, which are described in the following sections, are implemented in the "asciidoctor-idris2" add-on.¶
Idris2 shares with Haskell and other Haskell relatives built-in support for literate programming. We use the Bird mode which marks lines of code with a '>' symbol in the leftmost column. The literate programming rule that states that a block of code must always be separated from normal text by at least one blank line applies.¶
The following example contains a block of two lines of Idris2 code:¶
Some text > a : Int > a = 2 More text¶
Note that the '>' symbol is also used by AsciiDoc as an alternate way of defining a blockquote which is consequently not available in a computerate specification. The normal syntax for blockquotes must be used instead.¶
The code will not appear in the rendered document, but self-inclusion can be used to copy part of the code into the document, thus guaranteeing that this code is verified by the type-checker:¶
> -- tag::currying[] > total > currying : ((a, b) -> c) -> (a -> b -> c) > currying f = \x => \y => f (x, y) > -- end::currying[] .... include::myfile.lidr[tag=currying] ....¶
Because Idris2 does not resolve forward references by default, self-inclusion can also be used to reorder paragraphs when the flow of explanations does not coincide with the flow of the code.¶
Alternating paragraphs of text and code permits to keep both representations as close as possible and is an effective way to quickly discover that the code and the text are diverging. The convention is to insert the code beneath the text it is related to.¶
To be treated as a literate programming file, the AsciiDoc document must use the suffix ".lidr". This generally means that a document will be split in multiple documents, some with the ".adoc" extension and some with the ".lidr" extension. These files are put back together by using, directly or indirectly, AsciiDoc "include" statements in the files.¶
Using code macros in lieu of the equivalent constants in a document ensures that the text stays consistent during the development of the specification.¶
The type of the code passed to the macro must implement the Asciidoc
interface so it is converted into properly escaped Asciidoc.
Section 4.1.3 explains how to implement the Asciidoc
interface for user defined types.¶
A code macro searches first for an Asciidoc
implementation that has the same name than the back-end, then fallback to an unnamed implementation when a named implementation cannot be found.
This permits to use all the extensions specific to a particular back-end.¶
The code:[]
inline macro is used when the result is to be inserted as AsciiDoc inline text.¶
For instance the following excerpt taken from the computerate specification of [RFC8489]:¶
> retrans' : Nat -> Int -> Maybe (List1 Int) > retrans' rc = fromList . take rc . scanl (+) 0 > . unfoldr (bimap id (*2) . dup) > retrans : Nat -> Int -> String > retrans rc = maybe "Error" > (foldr1By (\e, a => show e ++ " ms, " ++ a) > (\x => "and " ++ show x ++ "ms")) . retrans' rc > timeout : Nat -> Int -> Int -> String > timeout rc rto rm = maybe "Error" > (\e => show (last e + rm * rto)) (retrans' rc rto) > rc : Nat; rc = 7 > rto : Int; rto = 500 > rm : Int; rm = 16 For example, assuming an RTO of code:[rto]ms, requests would be sent at times code:[retrans rc rto]. If the client has not received a response after code:[timeout] ms, the client will consider the transaction to have timed out.¶
is rendered as¶
"For example, assuming an RTO of 500ms, requests would be sent at times 0 ms, 500 ms, 1500 ms, 3500 ms, 7500 ms, 15500 ms, and 31500ms. If the client has not received a response after 39500 ms, the client will consider the transaction to have timed out."¶
The "code::[]"
block macro (notice the double colon) is used to generate AsciiDoc blocks in a way similar to the inline code macro.¶
The API documentation (IdrisDoc) generator in Idris has been extended to generate AsciiDoc instead of HTML. An Asciidoctor include processor has been added to build and integrate that generated document as part of the document rendering.¶
For instance, the following generates the IdrisDoc for the asciidoc.ipkg package and includes the output in the document:¶
include::asciidoc.ipkg[leveloffset=+2]¶
The document is generated with the main section at level one so the "leveloffset" attribute is used to update the actual section level.¶
The code in a computerate specification uses the programming language [Idris2] in literate programming [Knuth92] mode. Although most programming languages could have been used, Idris2 has been chosen for the following features:¶
The most important of these features are totality checking and the dependent type system, which permit to ensure an high level of correctness to the code. Generating portions of a document from a programming language that lacks these features would only bring marginal improvements in the quality of a specification.¶
The next sections describe an Idris2 package that can be used to simplify the generation of IdrisDoc. Appendix B lists the API for that same package.¶
The Asciidoc
module provides a way to programmatically build an AsciiDoc fragment without having to worry about the particular formatting details.¶
The elements of an AsciiDoc document are grouped in 4 categories:¶
Content
is the sum type of the possible parts that compose an AsciiDoc text:¶
TextContent
: BreakContent
: ItalicContent
: LinkContent
: IndexContent
: BoldContent
: SubscriptContent
: SuperscriptContent
: MonospaceContent
: CrossrefContent
: PassContent
:
OtherContent
is used to extend the Content sum type with content that is specific to a backend.¶
Block
is the sum type of the possible blocks that compose an AsciiDoc document:¶
ParagraphBlock
: LiteralBlock
: ImageBlock
: SourceBlock
: SidebarBlock
: QuoteBlock
: DefinitionListBlock
: OrderedListBlock
: UnorderedListBlock
: TableBlock
: IndexBlock
: PassBlock
:
OtherBlock
is used to extend the Block sum type with blocks that are specific to a backend.¶
User-defined Idris2 types can implement the Asciidoc
interface to streamline their conversion into AsciiDoc, in a way that is similar to the use of the standard Show
and Pretty
interfaces.¶
The Asciidoc
interface defines two functions, contents
and blocks
which, after implementation, generates respectively a non-empty list of Content
instances or a non-empty list of Block
instances.
The former is called when using an inline code macro, the latter when using a block code macro.
Both functions are implemented by default so it is mandatory to implement only one of the two.¶
For example the following fragment defines how to render the result of a decision function in a specification:¶
> Asciidoc (Dec a) where > contents (Yes prf) = singleton (TextContent "yes") > contents (No contra) = singleton (TextContent "no") Is 1 + 1 = 2? code:[decEq (1 + 1) 2]. + Is 1 + 1 = 3? code:[decEq (1 + 1) 3].¶
The Asciidoc
interface can be implemented multiple times using named implementations.
This is used to generate different content or block.¶
The Asciidoc
interface is implemented for the builtin types String
, Char
, Integer
, Int
, Int8
, Int16
, Int32
, Int64
, Bits8
, Bits16
, Bits32
, Bits64
, and Double
.¶
The "asciidoctor-idris2" must know if an implementation of the Asciidoc
is available on a separate package.
These package dependencies must be added to the document header attribute ":idris2-packages:", separated by spaces or a comma.
The "contrib" and "asciidoc" packages are always added as dependencies, and so do not need to be listed in the ":idris2-packages:" attribute.¶
Additional packages containing implementations of the Asciidoc
interface that are useful when writing an Internet-Draft will be documented in separate documents.¶
This module supplements the Asciidoc
module with types that implement the AsciiDoc extensions specific to the "xml2rfc" Asciidoctor backend.¶
CrossrefXml2rfc
extends the Crossref
content with additional attributes¶
LinkXml2rfc
extends the Link
content with additional attributes¶
Bcp14
is an additional content.¶
Comment
is an additional content.¶
Unicode
is an additional content.¶
ParagraphXml2rfc
extends the Paragraph
block with additional attributes¶
LiteralXml2rfc
extends the Literal
block with additional attributes¶
ImageXml2rfc
extends the Image
block with additional attributes¶
SourceXml2rfc
extends the Source
block with additional attributes¶
Alt
is an additional block.¶
Figure
is an additional block.¶
DefinitionListXml2rfc
extends the DefinitionList
block with additional attributes¶
OrderedListXml2rfc
extends the OrderedList
block with additional attributes¶
UnorderedListXml2rfc
extends the UnorderedList
block with additional attributes¶
TopSection
is the sum type of the possible top-level sections that compose an AsciiDoc document:¶
Note
is an additional top-level section.¶
Document
represents a complete AsciiDoc document.¶
A computerate specification can be converted into an informal specification with the "computerate" command that is distributed as a Docker image that can be built as follow:¶
docker build git://shalmaneser.org/yathewEngod7#0.0 -t computerate¶
An AsciiDoc file can then be converted with the following command:¶
docker run --rm -v $(pwd):/workspace computerate <file>¶
Note that only the files in the repository and sub-repositories where the command is executed are visible to that command. That means that files or symbolic links to files outside that hierarchy cannot be used. On the other hand external directories mounted with the "--bind" option can be used.¶
The "computerate" command is configured to include the following Asciidoctor add-ons:¶
The following diagram generators are available for use by asciidoctor-diagram:¶
The following additional Idris2 packages are installed in the Docker image:¶
An Idris2 package to generate a document, an embeddable document, or an inline document in AsciiDoc.¶
A module that defines types for the generic AsciiDoc syntax.¶
Alignment.¶
Things that have an AsciiDoc representation.¶
Implemented by String, Char, Integer, Int, Int8, Int16, Int32, Int64, Bits8, Bits16, Bits32, Bits64, Double, List1.¶
Types of blocks.¶
Types of inline content.¶
A cross-reference content.¶
A definitition list.¶
A definition term.¶
An image.¶
An index term content¶
A list or table cell.¶
A link content.¶
Literal.¶
Unordered list label style.¶
Ordered list label type.¶
An ordered list.¶
A paragraph.¶
Passthrough.¶
A quote.¶
(id : Maybe String) -> (cite : Maybe String) -> (quotedFrom : Maybe String) -> (content : Either (List1 Block) (List1 Content)) -> Quote¶
A table row.¶
A sidebar,¶
A table.¶
(id : Maybe String) -> (title : Maybe (List Content)) -> (align : Maybe Align) -> (head : Maybe (List1 Row)) -> (body : List1 Row) -> (foot : Maybe (List1 Row)) -> Table¶
An unordered list.¶
A Module that defines types for the AsciiDoc extensions of the "xml2rfc" back-end.¶
Intended category.¶
Intellectual Property Rights.¶
Intended stream.¶
Types of top sections.¶
Converts a Document into an Asciidoc document.¶
No technology that cannot explain its own results (LLM, AI/ML) have been involved in the creation of this document or its associated tooling.¶
Stephane is a co-founder of the Nephelion project, project that started back in 2014 during a week-end visiting national parks in Utah. Computerate Specifying is the successor of this project, and it could not have been done without the frequent reviews and video calls with Stephane during these last 10 years.¶
This section is to be removed before publishing as an RFC.¶
Document:¶
Tooling:¶