Mal in Coq?

[opain-replika]

Title pretty much.
Placeholder for a solution :D
Why do you think mal, despite being written in all sorts of, inclufing obscure, languages still doesn't have a coq implementation?

There may be some issue in running mal in pure coq, as it was not really intended[citacion needed], and may be even counter productive as it doesn't have a "usable-ish enough" IO functionality.

Coq programs however can be exported into other languages, for example: Ocaml, R5RS, and adapted using those. The benefit of using coq for mal may be:

• design, spec verification;
• set basis of verified implementation stepping up it's implementation standard;
• may improve program and library reusability;
• Mal can become somewhat more or less production ready? 😅
  Even if it isn't really a project goal, I'm curious to hear your opinion.

[opain-replika]

If I could, I would. instead of opening the issue.