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

[Sean Charles (emacstheviking)]

IT was a long shit! 

:D

However, the fruits of my exploration this morning are such that I have now become interested in Coq, like I need more distractions.

THanks


> On 2 May 2022, at 13:25, Julien Fischer <jfischer at opturion.com> wrote:
> 
> 
> 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.