It doesn't seem as full-featured as other systems at this point. For instance, there doesn't seem to be code generation to go from the proven code to another la

It doesn't seem as full-featured as other systems at this point. For instance, there doesn't seem to be code generation to go from the proven code to another language (like Rocq, formerly Coq, and others can do).