Praise Obj.magic! It keeps bailing me out of Coq extraction problems.

@lyxia Could you show an example of code that Coq proved to be Obj.magic-safe?

Just to be clear, I'm using Obj.magic in unverified ways. To actually verify OCaml, I've only heard of GOSPEL a week ago, that I haven't tried so I even don't know if it can answer your question.

@lyxia I thought you are talking about Obj.magic in the code generated by Coq. I'm going to look into gospel, thanks.

Sign in to participate in the conversation
La Quadrature du Net - Mastodon - Media Fédéré

The social network of the future: No ads, no corporate surveillance, ethical design, and decentralization! Own your data with Mastodon!