Lessness (Oct 08 2022 at 20:45): Lessness (Oct 08 2022 at 20:45):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?
Karl Palmskog (Oct 08 2022 at 20:49):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
Huỳnh Trần Khanh (Oct 09 2022 at 00:53):(deleted)
Lessness (Oct 09 2022 at 12:33):CoqAsm has disappeared as (complete) source code corresponding to the article, right? :sob:
I will take a look at Bedrock2, big thank you!
Karl Palmskog (Oct 09 2022 at 12:37):historical archive here, not usable with recent Coq: https://github.com/nbenton/x86proved
Karl Palmskog (Oct 09 2022 at 12:48):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: Apr 19 2024 at 00:02 UTC