coq-simple-io VS UniMath

My point about a proof assistant language, let's just say Coq, is focused on pure, referentially transparent functions. There are no IORef like escape hatches required to make things work, although you could probably argue that stuff like this is still pure as, there are certainly escape hatches. Generally speaking, in proof assistants, the program can be self-contained, and is thus "pure".

It's possible to do all that work still in Coq, so that the extracted code can directly be compiled into an executable. One way is to use the coq-simple-io library, which basically wraps the OCaml standard library (including functions for reading and writing files/stdin/stdout) as Coq axioms. For example, I did extraction that way in a previous iteration of AoC: https://github.com/Lysxia/advent-of-coq-2018/blob/master/sol/day01_1.v

For those interested in formalisation of homotopy type theory, there are several (more or less) active and developed libraries. To mention a few:

UniMath (https://github.com/UniMath/UniMath, mentioned in the article)

Coq-HoTT (https://github.com/HoTT/Coq-HoTT)

agda-unimath (https://unimath.github.io/agda-unimath/)

cubical agda (https://github.com/agda/cubical)

All of these are open to contributions, and there are lots of useful basic things that haven't been done and which I think would make excellent semester projects for a cs/math undergrad (for example).

I just wonder if there are any irl meetups of people involved with formalizing mathematics, I thought that it would be a cool hobby to pick up (with some background in math and programming) but the existing libraries, like MathLib, TypeTopology or UniMath look a bit intimidating...