Formality is an upcoming proof/programming language that combines optimal reductions with dependent types, theorem proving and so on. When I last posted about it, I told you the project was an experiment that wasn't really meant to be used yet. The amount of things that have been done in the last months is so huge that, at this point, I'm proud to say it is actually usable... ish. There is still a lot to do until we reach the levels of Agda, Idris, etc., but, regardless, we already have a great working language with documentation, a nice CLI, typed holes, helpful error messages, a readable syntax and so on.
So, if you find some time, please download it and have some fun proving stuff and getting your mind blown by elementary affine logic, self types, runtime fusion and so on! We're even trying to figure out how to implement higher inductive types with Self (which is slightly complicated by the fact I don't know much about them yet, but, from what I've heard, seems like Self Types are enough!?).
Our docs: http://docs.formality-lang.org
Main repo: https://github.com/moonad/formality
Telegram group: https://t.me/formality_lang
Will be delighted to hear about your experience with it!