Stream: wg-secure-code

Topic: hacspec


Tony Arcieri (Jan 06 2020 at 04:30, on Zulip):

This is pretty interesting: https://twitter.com/bascule/status/1213937672676356096

Shnatsel (Jan 07 2020 at 00:20, on Zulip):

Oooh, that's pretty cool

franziskus (Jan 14 2020 at 13:25, on Zulip):

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:

Alex Gaynor (Jan 14 2020 at 13:27, on Zulip):

Is this the next step of HACL*?

franziskus (Jan 14 2020 at 13:29, on Zulip):

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

franziskus (Jan 14 2020 at 13:30, on Zulip):

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: )

Last update: Jan 28 2020 at 00:35UTC