This is pretty interesting: https://twitter.com/bascule/status/1213937672676356096
hacspec-rust: reference specifications of various cryptographic algorithms written in a subset of @rustlang: https://github.com/hacspec/hacspecs-rust/tree/master/src- Tony “Abolish ICE” Arcieri 🦀 (@bascule)
Oooh, that's pretty cool
We're still in pretty early stages here. But I hope we have something to show in a couple months, i.e. a proper formalisation and a comprehensive hacspec library. But let me know if you're interested in helping :slight_smile:
Is this the next step of HACL*?
We want to be able to generate the specs in HACL* from this, yes. So it's not replacing HACL* but should make it easier to write the specs that are used as starting point for the correctness proofs
ideally we want more than only F* as target though. cryptol and coq for example would be nice (in case someone is interested in writing those compilers :smiley: )