Update the README

2 files changed, 64 insertions, 2 deletions

diff --git a/README.md b/README.md
index 74b081e6..97c6bd86 100644
--- a/README.md
+++ b/README.md
@@ -1,2 +1,64 @@
-# aeneas
-From Rust to pure programs
+<p><div style="text-align: center">
+<img src="static/Aeneas.jpg"
+     alt="Lapyx removing arrowhead from Aeneas" title="Lapyx removing arrowhead from Aeneas"
+     style=""/>
+<figcaption>
+Unknown author, <i>Lapyx removing arrowhead from Aeneas</i> [Fresco].
+Wall in Pompei, digital image from Michael Lahanis.
+<a href="https://commons.wikimedia.org/w/index.php?curid=1357010">Source</a>
+</figcaption>
+</div></p>
+
+# Aeneas
+
+Aeneas is a compiler from LLBC, a language inspired by Rust's MIR, to pure lambda calculus.
+It is meant to be used on the output produced by [Charon](https://github.com/Kachoc/charon),
+which compiles Rust programs to LLBC, to allow the verification of Rust propgrams in
+proof assistants. It currently has a backend for the [F\*](https://www.fstar-lang.org)
+theorem prover, and we intend to add backends for other provers such as Coq, HOL4 or LEAN.
+
+## Project Structure
+
+- `src`: the OCaml sources. Note that we rely on Dune to build the project.
+- `fstar`: F\* files providing basic definitions and notations for the code
+  generated for F\*.
+- `tests`: files generated by applying Aeneas on some of the test files of Charon,
+  completed with hand-written files (proof scripts, mostly).
+- `rust-tests`: miscelleanous files, to test the semantics of Rust or generate
+  code in a one-shot manner (mostly used for the arithmetic definitions, for
+  instance to generate `MIN` and `MAX` constants for all the integer types
+  supported by Rust).
+
+## Usage
+
+The simplest way to run Aeneas is to execute `dune exec -- src/main.exe [OPTIONS] LLBC_FILE`,
+where `LLBC_FILE` is an .llbc file generated by Charon.
+
+Aeneas provides a lot of flags and options to tweak its behaviour: you can use `--help`
+to display a detailed documentation.
+
+## Targeted Subset And Current Limitations
+
+We target **safe** Rust.
+
+We have the following limitations, that we plan to address one by one:
+
+- no loops: ongoing work. We are currently working on a "join" operation on
+  environments to address this issue.
+- no functions pointers/closures/traits: ongoing work.
+- limited type parametricity: it is not possible for now to instantiate a type
+  parameter with a type containing a borrow. This is mostly an engineering
+  issue. We intend to quickly address the issue for types (i.e., allow `Option<&T>`),
+  and later address it for functions (i.e., allow `f<&T>` - we consider this to
+  be less urgent).
+- no nested borrows in function signatures. We might allow nested borrows
+  while forbiding what we call "borrow overwrites" (see the paper) as a first
+  step towards supporting this feature.
+- no interior mutability: long-term effort. Interior mutability introduces
+  true aliasing: we will probably have to combine our pure lambda calculus
+  with separation logic to address this.
+  Note that interior mutability is mostly anecdotical in sequential execution,
+  but necessary for concurrent execution (it is exploited by the synchronisation
+  primitives).
+- no concurrent execution: long-term effort. We plan to address coarse-grained
+  parallelism as a long-term goal.
diff --git a/static/Aeneas.jpg b/static/Aeneas.jpg
new file mode 100644
index 00000000..6dbc9988
--- /dev/null
+++ b/static/Aeneas.jpg