diff --git a/docs/preface.md b/docs/preface.md new file mode 100644 index 0000000000..e41e8b0f9e --- /dev/null +++ b/docs/preface.md @@ -0,0 +1,238 @@ +--- +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? +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, +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. + +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 are 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 (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 +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 are sometimes 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 are 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 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, +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.