[m-users.] CompCert C as a backend for Mercury ?

Julien Fischer jfischer at opturion.com
Mon May 2 22:25:50 AEST 2022


On Mon, 2 May 2022, Sean Charles (emacstheviking) wrote:

> Today I learned of:   https://compcert.org/
> 
> A formally verified C compiler. I wondered what exposure it has to the
> erudite members of this thread, and more to the point, has anybody
> tried to compile the output of the mercury compiler with it?

Not to my knowledge.  I was aware of its existence, but since its
license does not allow commercial use and one of the things I do with
Mercury is develop commercial software there didn't seem any compelling
reason to look into it further.

> It would seem like a match made in heaven.
> 
> I will be downloading this compiler to see what I can do with it.

Just so you're aware: there's bit more to it than just doing

     $ ./configure --with-cc=ccomp

If you search the git repository for when we added support for clang**
(circa 2011), that might give you some idea of what is required to use
a new C compiler.

The obvious starting point is: can you successfully compile the Boehm
GC with it?

Julien.


More information about the users mailing list