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):

There isn't documentation though. This means that I should take a look at the source code to learn how to use it right?

I mean, I'm not averse to reading code. It's just that I'm asking if I'm missing something.

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: Jan 27 2023 at 02:04 UTC