Viewing profile — _thejanus_

I think so! You can codegen Ocaml directly, which means you have the benefit of lots of nice compiler libs and tools right out of the gate, but the metatheory is also expressive en…

What do you mean by this? I don’t want to be annoying and throw “propositions-as-types” at you, but as I understand it, F* is very much already doing this. Its type system is the p…

Yes, I’ve used the EverParse lib, as well as low* extensively! I found a really nice use case, low* makes writing bare metal protocol parsers incredibly easy and compositional at n…