doc: update the README

README.md

@@ -1,10 +1,12 @@
 # <img src="logo.png" alt= "logo" width="120px" height="120px" style="vertical-align: middle;"> <span style="vertical-align: middle;">coq-of-rust</span>
 
-> Formal verification for Rust 🦀 by translation to the proof system Coq 🐓
+> Formal verification tool for Rust 🦀
 
-*⚠️ Still a work in progress! ⚠️*
+Made by [🌲&nbsp;Formal Land](https://formal.land/)
 
-https://formal.land/
+Formal verification enables the making of software without bugs by showing that it follows a precise specification and covers all execution cases.
+
+`coq-of-rust` is a formal verification tool for Rust that translates the code to the [proof system Coq 🐓](https://coq.inria.fr/). See our blog post [Verifying an ERC-20 smart contract in Rust](https://formal.land/blog/2023/12/13/rust-verify-erc-20-smart-contract) to have an example of verified Rust code.
 
 ## Table of Contents
 
@@ -16,35 +18,52 @@ https://formal.land/
 - [Alternative Projects](#alternative-projects)
 - [Contributing](#contributing)
 
+## Example
+The heart of `coq-of-rust` is the translation of Rust code to Coq. Once some Rust code is translated to Coq, it can then be verified using standard proof techniques. Here is an example of a Rust function translated to Coq:
+```rust
+fn add_one(x: u32) -> u32 {
+    x + 1
+}
+```
+translates in Coq to:
+```coq
+Definition add_one (x : u32.t) : M u32.t :=
+  let* x := M.alloc x in
+  let* α0 : u32.t := M.read x in
+  BinOp.Panic.add α0 ((Integer.of_Z 1) : u32.t).
+```
+
 ## Rationale
-Formal verification allows to prevent all bugs in critical software. This is used in aerospace industry for example 🧑‍🚀.
+Formal verification allows the prevention of all bugs in critical software. This is used in the aerospace industry, for &nbsp;🧑‍🚀.
 
 The type system of Rust already offers strong guarantees to avoid bugs that exist in C or Python. We still need to write tests to verify the business rules or the absence of `panic`. Testing is incomplete as it cannot cover all execution cases.
 
-With formal verification we cover all cases (code 100% bug-free!). We replace the tests by mathematical reasoning on code. You can view it as an extension of the type system, but without restrictions on the expressivity.
+With formal verification, we cover all cases (code 100% bug-free!). We replace the tests with mathematical reasoning on code. You can view it as an extension of the type system but without restrictions on the expressivity.
 
-This tool `coq-of-rust` translates Rust programs to the formal verification language Coq to make Rust programs 100% safe 🌙.
+This tool `coq-of-rust` translates Rust programs to the formal verification language Coq to make Rust programs 100% safe&nbsp;🚀.
 
 ## Prerequisites
 
-- Rust (latest stable version)
+- Rust
 - Coq (version 8.14 or newer)
 
-## Details
-The translation works at the level of the [HIR](https://rustc-dev-guide.rust-lang.org/hir.html) intermediate representation of Rust.
+## Install
 
-From the root of this repository, run:
+From the root of this repository, install `coq-of-rust` with:
 
 ```sh
 cargo install --path lib/
 ```
 
-Then in any Rust project, to generate a `Crate.v` file with the Coq translation of the crate:
+Then, in any Rust project, generate a `Crate.v` file with the Coq translation of the crate:
 
 ```sh
 cargo coq-of-rust
 ```
 
+## Details
+The translation works at the level of the [THIR](https://rustc-dev-guide.rust-lang.org/thir.html) intermediate representation of Rust.
+
 Translate the test files (but show the error/warning messages):
 
 ```sh
@@ -65,23 +84,31 @@ cd CoqOfRust
 make
 ```
 
-## Features
-Note that we are still developing support for most of language constructs of Rust.
+## Language features
+We support 80% of the Rust examples from the [Rust Book by Examples](https://doc.rust-lang.org/rust-by-example/). This includes:
 
-- translation of a single Rust file to Coq
-- translation of a whole crate project
+- basic control structures (like&nbsp;`if` and&nbsp;`match`)
+- loops (`while` and&nbsp;`for`)
+- references and mutability (`&` and&nbsp;`&mut`)
+- closures
+- panics
+- user types (with&nbsp;`struct` and&nbsp;`enum`)
+- the definition of traits
+- the implementation keyword&nbsp;`impl` for traits or user types
 
-## Limitations
-This project is still early stage. We focus for now on the translation of a purely functional subset of Rust, and then will add a monadic system to support memory mutations.
+## Contact
+For formal verification services on your Rust code base, contact us at [&#099;&#111;&#110;&#116;&#097;&#099;&#116;&#064;formal&#046;&#108;&#097;&#110;&#100;](mailto:contact@formal.land). Formal verification can apply to smart contracts, database engines, or any critical Rust project. This provides the highest confidence level in the absence of bugs compared to other techniques, such as manual reviews or testing.
 
 ## Alternative Projects
 
 Here are other projects working on formal verification for Rust:
 
-- [Aeneas](https://github.com/AeneasVerif/aeneas): Translation from MIR to purely functional Coq/F* code
+- [Aeneas](https://github.com/AeneasVerif/aeneas): Translation from MIR to purely functional Coq/F* code. Automatically put the code in a functional form. See their paper [Aeneas: Rust verification by functional translation](https://dl.acm.org/doi/abs/10.1145/3547647).
 - [Hacspec v2](https://github.com/hacspec/hacspec-v2): Translation from THIR to Coq/F* code
 - [Creusot](https://github.com/xldenis/creusot): Translation from MIR to Why3 (and then SMT solvers)
 - [Kani](https://github.com/model-checking/kani): Model-checking with [CBMC](https://github.com/diffblue/cbmc)
 
 ## Contributing
-Open pull-requests or issues to contribute to this project. All contributions are welcome! This project is open-source under license AGPL for the Rust code (the translator) and MIT for the Coq libraries. There is a bit of code taken from the [Creusot](https://github.com/xldenis/creusot) project, to make the Cargo command `coq-of-rust` and run the translation in the same context as Cargo.
+This is all open-source software.
+
+Open some pull requests or issues to contribute to this project. All contributions are welcome! This project is open-source under license AGPL for the Rust code (the translator) and MIT for the Coq libraries. There is a bit of code taken from the [Creusot](https://github.com/xldenis/creusot) project to make the Cargo command `coq-of-rust` and run the translation in the same context as Cargo.