Merge pull request #16 from input-output-hk/abailly-iohk/introduce-adrs

Introduce ADRs to keep track of our main decisions

README.md

@@ -13,6 +13,8 @@ This repository is intended to host more or less formal specifications, experime
 * [Logbook](Logbook.md) contains a detailed account of problems,
   successes, failures, ideas, references and is intended as a tool to
   help the team members stay in sync
+* We document our main design and architecture decisions along the way
+  using [Architectural Decision Records](./docs/adr).
 
 ## Hacking
 

docs/adr/001-record-architectural-decisions.md

@@ -0,0 +1,26 @@
+---
+slug: 1
+title: |
+  1. Record Architecture Decisions
+authors: []
+tags: [Accepted]
+---
+
+## Status
+
+Accepted
+
+## Context
+
+We are in search for a means to describe our technical architecture.
+
+We are a small team working in a lean and agile way, so we naturally prefer also light-weight documentation methods which also accomodate change easily.
+
+## Decision
+
+* We will use _Architecture Decision Records_, as described by Michael Nygard in this [article](http://thinkrelevance.com/blog/2011/11/15/documenting-architecture-decisions).
+* We will follow the convention of storing those ADRs as Markdown formatted documents stored under `docs/adr` directory, as exemplified in Nat Pryce's [adr-tools](https://github.com/npryce/adr-tools). This does not imply we will be using `adr-tools` itself.
+
+## Consequences
+
+See Michael Nygard's article, linked above.

docs/adr/002-generate-interfaces-from-agda.md

@@ -0,0 +1,27 @@
+---
+slug: 2
+title: |
+  2. Formal model in Agda is ground truth
+authors: []
+tags: [Accepted]
+---
+
+## Status
+
+Accepted
+
+## Context
+
+* We are striving to build a "trail of evidence" from the abstract and formal work of researchers describing the algorithm in written words, to the actual implementation written in some programming language
+* This trail starts at the formalisation of the algorithm and the various data structures, properties, components involved in a formal specification language namely [Agda](https://github.com/agda/agda)
+* In order to ensure consistency across various tools and experiments while working on simulations, prototypes, test environments, etc. we need a "common language" from which to derive actual, language-specification implementations.
+
+## Decision
+
+* We will consider Agda code as our _source of truth_ to define types, data structures and properties relevant to the implementation of the Peras algorithm
+
+## Consequences
+
+* Actual data structures for particular languages (eg. Haskell or Rust) should be _generated_ from Agda code
+* To simplify development, generated code can be checked in, properly packaged, and versioned to be used as a dependency by other components
+* Generated code must _never_ be manually modified

docs/adr/README.md

@@ -0,0 +1,4 @@
+# Architecture Decision Records
+
+1. [Use ADRs](001-record-architectural-decisions.md)
+2. [Agda is ground truth](002-generate-interfaces-from-agda.md)