Skip to content

Commit

Permalink
update README
Browse files Browse the repository at this point in the history
  • Loading branch information
nikomatsakis committed Mar 20, 2023
1 parent 959f352 commit ca14d99
Showing 1 changed file with 3 additions and 14 deletions.
17 changes: 3 additions & 14 deletions README.md
Original file line number Diff line number Diff line change
Expand Up @@ -6,21 +6,10 @@ and develop it as an official part of the language definition.

## Quickstart guide

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

## Tool

For the time being, the model is implemented in [PLT Redex](https://redex.racket-lang.org/).
PLT Redex was chosen because it is ridiculously accessible and fun to use.
It lets you write down type system rules and operational semantics and then execute them,
using a notation that is very similar to what is commonly used in published papers.
You can also write collections of unit tests and fuzz your model by generating test programs automatically.

The hope is that PLT Redex will prove to be a sufficiently accessible tool
that many Rust contributors will be able to understand, play with, and extend the model.

One downside of PLT Redex is that it doesn't scale naturally to performing proofs.
We may choose to port the model to another system at some point, or maintain multiple variants.
* Clone
* `cargo test --all`

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

0 comments on commit ca14d99

Please sign in to comment.