Since CompCert isn't free software, I don't have money for its potentially commercial use, and I'm procrastinating...
I am reading this article of 2013: https://www.microsoft.com/en-us/research/wp-content/uploads/2016/12/coqasm.pdf
Has someone tried to use it or something similar for programming?
some pieces of that project that live on here: https://github.com/coq-community/bits
If you are looking for languages that can be compiled from a Coq representation to ISA (assembly) level, Bedrock2 might be of interest: https://github.com/mit-plv/bedrock2
CoqAsm has disappeared as (complete) source code corresponding to the article, right? :sob:
I will take a look at Bedrock2, big thank you!
historical archive here, not usable with recent Coq: https://github.com/nbenton/x86proved
the reality is that most [new] Coq code that gets published is write-once-and-never-maintain. In some cases it's quite easy to port to recent Coq (e.g., when written in idiomatic SSReflect+MathComp), and sometimes it's really hard (e.g., for projects before 8.5 such as this)
Last updated: Sep 30 2023 at 07:01 UTC