Oh, didn't know that they are working on this.

https://github.com/coq/ceps/blob/coq-roadmap/text/069-coq-ro... and, of course, https://news.ycombinator.com/item?id=38779480

069-coq-roadmap.md? Oh, you!

So now we've got Rocq and Roc https://www.roc-lang.org/