Add bibliography

docs/README.md

@@ -19,10 +19,12 @@ The ReadTheDocs theme can be installed in virtual environment using pip as follo
 python3 -m venv juvixdocs_venv
 source juvixdocs_venv/bin/activate
 pip install --upgrade pip
+pip install sphinx-autobuild
 pip install sphinx_rtd_theme
 pip install myst_parser
 pip install sphinx_proof
 pip install sphinxcontrib-tikz
+pip install sphinxcontrib-bibtex
 ```
 
 ### LaTeX

docs/requirements.txt

@@ -1,4 +1,6 @@
 sphinx_rtd_theme
 myst-parser
 sphinx_proof
-sphinxcontrib-tikz
+sphinxcontrib-tikz
+sphinxcontrib-bibtex
+sphinx-autobuild

docs/source/conf.py

@@ -47,7 +47,8 @@
     "sphinx_rtd_theme",
     "myst_parser",
     "sphinx_proof",
-    "sphinxcontrib.tikz"
+    "sphinxcontrib.tikz",
+    "sphinxcontrib.bibtex"
 ]
 
 # Add any paths that contain templates here, relative to this directory.
@@ -191,6 +192,7 @@
 # If false, no module index is generated.
 #latex_domain_indices = True
 
+bibtex_bibfiles = ['refs.bib']
 
 # -- Options for manual page output ---------------------------------------
 

docs/source/motivation.md

@@ -4,11 +4,8 @@ Selected out by the twin Darwinian reapers of language network-effect path-depen
 
 This sorry result is overdetermined & difficult to precisely allocate causal responsibility for, but certainly a substantial contributor is the sheer difficulty and cost of formally verifying complex software systems. Most frequently, security is trial-and-error. At best, models are written and checked separately from the code, an expensive and error-prone process. An approach to security which can be expected to result in a different outcome must be constructive, unifying code & proofs into a single language, and must be compositional, so that sets of proofs can be imported & reused along with the libraries which comprise most of modern software. The approach must provide a typed language for succinct proofs which can tightly constrain the opaque behaviour of complex backend codebases, typecheckers which can be embedded by the manufacturers of user-facing software, such as web browsers, operating systems, or cybercoin wallets. The approach must reduce the costs of formally verifying software, and increase the legible user-facing benefits of doing so, to a degree where formal verification is the economically rational decision for networked software which handles sensitive data or the exchange of value.
 
-Smart contracts running on distributed ledgers are an archetypal example of a security-critical application, and one where the popular conceit of security-through-obscurity holds little sway, yet results so far have not been promising [@parity-wallet-postmortem] [@zero-ex-postmortem]. Luckily, the field has not yet been locked into particular technologies whose network effects could not be overcome, and the necessity of verifiable & verified software systems is widely-recognised. A radically different language is necessary: one that treats verifiability as a design problem, not a feature to be tacked on later, one that provides succinct, expressive, and composable proofs which can tightly constraint the behaviour of complex logic, and one that reduces the cost of verification to the point where not doing so for security-critical software will be considered simply irresponsible. Juvix aims to realise this ideal.
+Smart contracts running on distributed ledgers are an archetypal example of a security-critical application, and one where the popular conceit of security-through-obscurity holds little sway, yet results so far have not been promising {cite}`parity-wallet-postmortem` {cite}`zero-ex-postmortem`. Luckily, the field has not yet been locked into particular technologies whose network effects could not be overcome, and the necessity of verifiable & verified software systems is widely-recognised. A radically different language is necessary: one that treats verifiability as a design problem, not a feature to be tacked on later, one that provides succinct, expressive, and composable proofs which can tightly constraint the behaviour of complex logic, and one that reduces the cost of verification to the point where not doing so for security-critical software will be considered simply irresponsible. Juvix aims to realise this ideal.
 
 
-```{toctree}
----
-maxdepth: 1
----
+```{bibliography} refs.bib
 ```