Skip to content

Commit ca14d99

Browse files
committed
update README
1 parent 959f352 commit ca14d99

File tree

1 file changed

+3
-14
lines changed

1 file changed

+3
-14
lines changed

README.md

Lines changed: 3 additions & 14 deletions
Original file line numberDiff line numberDiff line change
@@ -6,21 +6,10 @@ and develop it as an official part of the language definition.
66

77
## Quickstart guide
88

9-
The quickstart guide can be found [in the documentation](https://nikomatsakis.github.io/a-mir-formality/docs/setup)
9+
Like any Rust project:
1010

11-
## Tool
12-
13-
For the time being, the model is implemented in [PLT Redex](https://redex.racket-lang.org/).
14-
PLT Redex was chosen because it is ridiculously accessible and fun to use.
15-
It lets you write down type system rules and operational semantics and then execute them,
16-
using a notation that is very similar to what is commonly used in published papers.
17-
You can also write collections of unit tests and fuzz your model by generating test programs automatically.
18-
19-
The hope is that PLT Redex will prove to be a sufficiently accessible tool
20-
that many Rust contributors will be able to understand, play with, and extend the model.
21-
22-
One downside of PLT Redex is that it doesn't scale naturally to performing proofs.
23-
We may choose to port the model to another system at some point, or maintain multiple variants.
11+
* Clone
12+
* `cargo test --all`
2413

2514
<!-- TODO -->
2615
<!-- ## Structure of the repository -->

0 commit comments

Comments
 (0)