Stream: Coq users

Topic: Coq and assembler


view this post on Zulip 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?

view this post on Zulip 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

view this post on Zulip Huỳnh Trần Khanh (Oct 09 2022 at 00:53):

(deleted)

view this post on Zulip 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!

view this post on Zulip Karl Palmskog (Oct 09 2022 at 12:37):

historical archive here, not usable with recent Coq: https://github.com/nbenton/x86proved

view this post on Zulip 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: Jun 13 2024 at 05:01 UTC