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.
The social network of the future: No ads, no corporate surveillance, ethical design, and decentralization! Own your data with Mastodon!