Update the README

1 files changed, 21 insertions, 20 deletions

diff --git a/README.md b/README.md
index 3acba834..31dc74f4 100644
--- a/README.md
+++ b/README.md
@@ -13,24 +13,18 @@ Wall in Pompei, digital image from Michael Lahanis.
 
 Aeneas is a verification toolchain for Rust programs.  It relies on a translation from Rusts's MIR
 internal language to a pure lamdba calculus.  It is intended to be used in combination with
-[Charon](https://github.com/Kachoc/charon), which compiles Rust programs to an intermediate
-representation called LLBC. It currently has backends for the [F\*](https://www.fstar-lang.org)
-theorem prover and the [Coq](https://coq.inria.fr/) proof assistant, and we intend to add 
-backends for other provers such as [HOL4](https://hol-theorem-prover.org/) or [LEAN](https://leanprover.github.io/).
+[Charon](https://github.com/AeneasVerif/charon), which compiles Rust programs to an intermediate
+representation called LLBC. It currently has backends for [F\*](https://www.fstar-lang.org),
+[Coq](https://coq.inria.fr/), [HOL4](https://hol-theorem-prover.org/) and [LEAN](https://leanprover.github.io/).
 
 ## Project Structure
 
 - `src`: the OCaml sources. Note that we rely on [Dune](https://github.com/ocaml/dune)
   to build the project.
-- `fstar`: F\* files providing basic definitions and notations for the
-  generated code (basic definitions for arithmetic types and operations,
-  collections like vectors, etc.).
+- `backends`: standard libraries for the existing backends (definitions for
+   arithmetic operations, for standard collections like vectors, theorems, tactics, etc.)
 - `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).
 
 ## Installation & Build
 
@@ -83,27 +77,34 @@ to display a detailed documentation.
 
 ## Targeted Subset And Current Limitations
 
-We target **safe** Rust.
+We target **safe** Rust. This means we have no support for unsafe Rust, though we plan to
+design a mechanism to allow using Aeneas in combination with tools targeting unsafe 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.
+- **loops**: no nested loops for now. We are working on lifting this limitation.
+- **no functions pointers/closures/traits**: ongoing work. We are actively working on this
+  and plan to have support soon.
 - **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<&mut T>`),
   and later address it for functions (i.e., allow `f<&mut T>` - we consider this to
   be less urgent).
 - **no nested borrows in function signatures**: ongoing work.
-- **no interior mutability**: long-term effort. Interior mutability introduces
-  true aliasing: we will probably have to use a low-level memory model to address
-  this issue.
-  Note that interior mutability is truely necessary for concurrent execution (it
-  is exploited to implement the synchronisation primitives).
+- **interior mutability**: ongoing work. We are thinking of modeling the effects of
+  interior mutability by using ghost states.
 - **no concurrent execution**: long-term effort. We plan to address coarse-grained
   parallelism as a long-term goal.
 
+## Backend Support
+
+We currently support F\*, Coq, HOL4 and Lean. We would be interested in having an Isabelle
+backend. Our most mature backends are Lean and HOL4, for which we have in particular
+support for partial functions and extrinsic proofs of termination (see
+`./backends/lean/Base/Diverge/Elab.lean` and `./backends/hol4/divDefLib.sig` for instance)
+and tactics specialized for monadic programs (see
+`./backends/lean/Base/Progress/Progress.lean` and `./backends/hol4/primitivesLib.sml`).
+
 ## Formalization
 
 The translation has been formalized and published at ICFP2022: [Aeneas: Rust