This might turn into it's own topic, but let me put it here for now.
There are currently (at least) two low level languages formalized in Coq, jasmin and bedrock2.
I'm wondering how they compare. @Jason Gross ?
https://github.com/mit-plv/fiat-crypto/issues/783
@Bas Spitters I don't have much interesting to say on this (I just replied to the issue). A good way of seeing how they compare might be seeing how much work it takes to port the bedrock2 backend for fiat-crypto to Jasmin
Last updated: Oct 13 2024 at 01:02 UTC