I was a bit surprised nobody’s tried a “verified” implementation in something like Coq/Idris/Agda (unless i missed one - I wasn’t familiar with all the language

I was a bit surprised nobody’s tried a “verified” implementation in something like Coq/Idris/Agda (unless i missed one - I wasn’t familiar with all the languages in the list). Might be a fun project!