From 8ad81663673818d32a7f354b80394326ee10a990 Mon Sep 17 00:00:00 2001 From: Jonathan Cubides Date: Mon, 10 Feb 2025 09:28:54 -0500 Subject: [PATCH 1/6] First version --- docs/preface.md | 242 ++++++++++++++++++++++++++++++++++++++++++++++++ 1 file changed, 242 insertions(+) create mode 100644 docs/preface.md diff --git a/docs/preface.md b/docs/preface.md new file mode 100644 index 00000000000..31b363f0d0c --- /dev/null +++ b/docs/preface.md @@ -0,0 +1,242 @@ +--- +icon: material/home +description: A work-in-progress specification for the Anoma protocol. +social: + cards: false +tags: + - preface +search: + exclude: true +--- + +# Preface + +The Anoma protocol specification is being developed as part of Anoma. +Figuratively speaking, +it is the blueprint of Anoma, +but then, how can the blueprint be part of the whole? +In first approximation, +we are spiraling up, +bootstrapping from what started out as +a write up of the idea of Anoma for a wider audience +and a prototype implementation loosely based on ... ideas written up. +Less prosaic, +we can make sense of specification as part of the whole +if we consider that +future iterations of the existing code base will be +influenced by the current specification, +and—vice versa—issues discovered while implementing Anoma, +based on the current specs, +provide feed-back for future specifications. +In summary, + +> _Anoma, as a whole, is in constant flux._ + +We fully embrace the dynamic and open nature of Anoma. +We thus offer an unmasked view of +the evolution of the Anoma protocol specification, +also referred to as _Anoma specs,_ +the document you are reading right now and here. + +We believe that accepting the principle of constant change +is a simple and honest approach to make sure that +there always will be potential for improvement. +To make this work, +we need to cope with the various stages of the evolution. +Thus, +we use [semantic versioning](https://semver.org/) to facilitate meaningful interactions, +be it questions on the forums, +PRs on the github repository, +or other ways of collaboration. + +!!! info "Constant improvement in three bullets" + + - Everything in this documentation may be subject to change. + This is an indispensable prerequisite of Anoma as a system + to adapt to changes in its environment. + + - The Anoma protocol specification is versioned to keep track of changes. + Thus, + if you want to ask a question, add a comment, or suggest improvements, + it is _indispensable_ to reference the **exact version** of the Anoma specs. + Please look at the website title or the footer of pages for + the version of the document—or + come back here to check whether we have new ways to indicate the version. + Should you want to reference the frequently changing + [`main` branch](https://github.com/anoma/nspec), + please provide a commit hash in place of a version number. + + - The Anoma protocol specification is written in English language. + However, + we also embed code snippets, + written in [juvix](https://juvix.org/). + The purpose of these code snippets is described [below](#use-of-juvix). + In short, + all of Anoma specs should be informative + without reference to the code. + + !!! note "" + + _Please let us know if the English language descriptions or not precise enough!_ + +### Purpose and scope + +Anoma specs describe the [[Protocol Architecture|protocol architecture]]. +In other words, +it provides a blueprint for how components of Anoma protocol instances +may interact to provide functionality. +Thus, +Anoma specs describe what any correct implementation +_has to_ provide and +_may provide._ +Anoma specs focus on the rules of the protocol, +not on any particular implementation +(even if we are concurrently working on an [implementation](https://github.com/anoma/anoma)). +How Anoma specs should relate to implementations—in general and in particular—is described +[below](#specification-natural-language-formal-languages-and-beyond). + +## Development, evolution, and growth + +Besides iterations and improvements of the existing specification, +new components will be added to the Anoma specs. +Roughly, +the table of contents will strictly grow, +not only in depth (detail), but also in length (encompass). +Whether and how ongoing research is to be incorporated into the Anoma specs is +being discussed on the [research forums](https://research.anoma.net/). +This is yet another facet of the principle of +constant evolution of Anoma's concepts and requirements. + +## Specification: natural language, formal languages, and beyond + +Let us recap what specifications are about, in general—not only about software specifications—to better understand what Anoma specs aim to provide. + +!!! quote "Specification [@Nissanke1999]" + + A specification primarily states what is required [for a task], + providing minimal or no details about how the task should be accomplished. + +This goal, i.e., capturing the requirements and essential structure, +can be achieved using English language. +However, +we sometimes are underestimating natural language's flexibility +to change meanings depending on the context, +which can catch us off guard. +We want to avoid any such haphazard ambiguities, +and thus, +in Anoma specs, +we use [formal languages](https://en.wikipedia.org/wiki/Formal_language), +as used and studied by logicians, mathematicians, and computer scientists. + +!!! quote "Mathematical expression of specifications" + + A formal specification is, in addition, + a mathematical expression of what is required (a computational task) + which may be subjected to mathematical scrutiny (reasoning or proof). + +Thus, +the main point of writing formal specification is additional precision, +which is often described as mathematical rigour.[^1] + +In summary, +Anoma specs use formal languages to complement natural language +and our list of requests is growing a second element: + +- _Please let us know if the English language descriptions or not precise enough!_ + +- _Please let us know if the formal specification does not match the English language descriptions!_ + +!!! todo "List and respond to requirements" + + We aim to list and address the functional requirements first, followed by the non-functional requirements. + +!!! todo "specs and implementation in detail" + +### Mathematical rigour, also for the implementation + +At some point in the future, +we may want to make sure that some given implementation matches the protocol, +i.e., demonstrate that an implementation is _correct_; +in short, +we want to _verify_ the implementation.[^2] +There is a large variety of methods, +which often are summarized as _[formal methods](https://en.wikipedia.org/wiki/Formal_methods),_ +which we may want to apply, now or in the future. +Note that formal _specification_ is of interest in and of itself: +it forces one to resolve any natural language ambiguities, +and in this way, +we also catch issues that tend to "hide" in natural language. + +In summary, +most concepts in the Anoma specs are intended to have formal counterparts +in what we *currently* call _idealized Anoma_ (v0.3-ish). +Anoma specs takes a page out of the proverbial book of formal methods, +but first and foremost, +the purpose of complementing English language prose with juvix code and formal languages +is mathematical rigour in the Anoma specs. + +## Use of Juvix + +Throughout the Anoma specs, +we embed code snippets, +written in [Juvix](https://juvix.org/). +While Juvix is still in its infancy, +compared to established languages like Coq, +Isabelle/HOL, Agda or Lean, +it serves our needs surprising well. +Let us highlight some aspects. + + +- A modern functional programming language with powerful features including + inductive types, pattern matching, and type classes for expressing + computational concepts clearly and concisely. For details, see the + [Essential Juvix](https://docs.juvix.org/0.6.9/tutorials/essential.html) + tutorial. + +- Support for hypertext documentation, including features such as clickable + references for easy code navigation. + +- An easy embedding into Lean4, which we use whenever juvix's type system restrictions + call for a more expressive language. + +- Built-in support for literate programming, enabling us to seamlessly blend + type definitions and function definitions with natural language explanations through + code snippets. This also provides robust type-checking capabilities for all + code snippets via [Juvix Markdown support](https://docs.juvix.org/), + ensuring that expressions are well-formed and type-safe. + +## Prerequisites + +The Anoma specs should be self-contained, ideally, +but this is rather a promise than a true statement. +For example, +almost certainly there are number technical terms that have become second nature to the authors that should be listed as pre-requisites, +but are not (yet). +Thus, +please reach out, +if you find that we use a term or concept that should at least be referenced +if not recapped in a footnote or note. +In particular, +we want the Anoma specs to grow into a source of information +for at least the following professionals: + +- Protocol designers and architects +- Implementation teams +- Verification experts +- External auditors + +Eventually, we want to reach the Anoma community at large. +So, +don't hesitate to join the discussion [Anoma](https://research.anoma.net/)! + +[^1]: Interestingly, Leslie Lamport goes as far as speaking of "writing math" + instead of "formally specifying". + +[^2]: Recall that this only makes sense for, + a specific version of the Anoma specs. \ No newline at end of file From 51800941d711c12a04cd312faaabf3d2f94c94a6 Mon Sep 17 00:00:00 2001 From: Jonathan Cubides Date: Mon, 10 Feb 2025 09:30:18 -0500 Subject: [PATCH 2/6] fix minor typos --- docs/preface.md | 8 ++++---- 1 file changed, 4 insertions(+), 4 deletions(-) diff --git a/docs/preface.md b/docs/preface.md index 31b363f0d0c..360888db574 100644 --- a/docs/preface.md +++ b/docs/preface.md @@ -21,7 +21,7 @@ but then, how can the blueprint be part of the whole? In first approximation, we are spiraling up, bootstrapping from what started out as -a write up of the idea of Anoma for a wider audience +a write-up of the idea of Anoma for a wider audience and a prototype implementation loosely based on ... ideas written up. Less prosaic, we can make sense of specification as part of the whole @@ -125,7 +125,7 @@ Let us recap what specifications are about, in general— [^2]: Recall that this only makes sense for, From 566cec0cd579de61c212e9d88ae6bde7549f96f8 Mon Sep 17 00:00:00 2001 From: Anthony Hart Date: Wed, 12 Feb 2025 02:37:46 -0500 Subject: [PATCH 4/6] Fix some typos --- docs/preface.md | 14 +++++++------- 1 file changed, 7 insertions(+), 7 deletions(-) diff --git a/docs/preface.md b/docs/preface.md index 1caff897025..e44dbd25ba4 100644 --- a/docs/preface.md +++ b/docs/preface.md @@ -24,7 +24,7 @@ bootstrapping from what started out as a write-up of the idea of Anoma for a wider audience and a prototype implementation loosely based on ... ideas written up. Less prosaic, -we can make sense of specification as part of the whole +we view the specification as part of the whole if we consider that future iterations of the existing code base will be influenced by the current specification, @@ -39,7 +39,7 @@ We fully embrace the dynamic and open nature of Anoma. We thus offer an unmasked view of the evolution of the Anoma protocol specification, also referred to as _Anoma specs,_ -the document you are reading right now and here. +the document you are reading right now. We believe that accepting the principle of constant change is a simple and honest approach to make sure that @@ -81,7 +81,7 @@ or other ways of collaboration. !!! note "" - _Please let us know if the English language descriptions or not precise enough!_ + _Please let us know if the English language descriptions are not precise enough!_ ### Purpose and scope @@ -148,7 +148,7 @@ In summary, Anoma specs use formal languages to complement natural language and our list of requests is growing a second element: -- _Please let us know if the English language descriptions or not precise enough!_ +- _Please let us know if the English language descriptions are not precise enough!_ - _Please let us know if the formal specification does not match the English language descriptions!_ @@ -216,7 +216,7 @@ Let us highlight some aspects. The Anoma specs should be self-contained, ideally, but this is rather a promise than a true statement. For example, -almost certainly there are number technical terms that have become second nature to the authors that should be listed as pre-requisites, +almost certainly there are a number of technical terms that have become second nature to the authors that should be listed as pre-requisites, but are not (yet). Thus, please reach out, @@ -238,5 +238,5 @@ don't hesitate to join the discussion [Anoma](https://research.anoma.net/)! [^1]: Interestingly, Leslie Lamport goes as far as speaking of "writing math" instead of "formally specifying". -[^2]: Recall that this only makes sense for, - a specific version of the Anoma specs. \ No newline at end of file +[^2]: Recall that this only makes sense for + a specific version of the Anoma specs. From b37b1c8f805abbc8a21db283f3fab5783fa2171e Mon Sep 17 00:00:00 2001 From: Anthony Hart Date: Thu, 13 Feb 2025 21:09:04 -0500 Subject: [PATCH 5/6] Corrections based on prior conversations --- docs/preface.md | 12 ++++-------- 1 file changed, 4 insertions(+), 8 deletions(-) diff --git a/docs/preface.md b/docs/preface.md index e44dbd25ba4..e7901e6d87c 100644 --- a/docs/preface.md +++ b/docs/preface.md @@ -18,13 +18,9 @@ search: Figuratively speaking, it is the blueprint of Anoma, but then, how can the blueprint be part of the whole? -In first approximation, -we are spiraling up, -bootstrapping from what started out as -a write-up of the idea of Anoma for a wider audience -and a prototype implementation loosely based on ... ideas written up. -Less prosaic, -we view the specification as part of the whole +We are bootstrapping; starting with a prototype implementation of +the idea of Anoma based on prior writings, intended for a wider audience. +We view the specification as part of the whole if we consider that future iterations of the existing code base will be influenced by the current specification, @@ -105,7 +101,7 @@ Besides iterations and improvements of the existing specification, new components will be added to the Anoma specs. Roughly, the table of contents will strictly grow, -not only in depth (detail), but also in length (encompass). +not only in depth (detail), but also in length (coverage). Whether and how ongoing research is to be incorporated into the Anoma specs is being discussed on the [research forums](https://research.anoma.net/). This is yet another facet of the principle of From 1aa882d37404f843ddfecfd1993ca1fa10eafe36 Mon Sep 17 00:00:00 2001 From: Anoma Research Date: Fri, 14 Feb 2025 02:11:37 +0000 Subject: [PATCH 6/6] Fix issues detected by pre-commit --- docs/preface.md | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/docs/preface.md b/docs/preface.md index e7901e6d87c..e41e8b0f9e2 100644 --- a/docs/preface.md +++ b/docs/preface.md @@ -18,7 +18,7 @@ search: Figuratively speaking, it is the blueprint of Anoma, but then, how can the blueprint be part of the whole? -We are bootstrapping; starting with a prototype implementation of +We are bootstrapping; starting with a prototype implementation of the idea of Anoma based on prior writings, intended for a wider audience. We view the specification as part of the whole if we consider that