This is much cooler than I thought it would be and calling it a proof language seems to undersell it. It seems to be more of a general purpose FP language that can compile to multiple backends and supports UI development out of the box (!!)
Also started with python, to avoid javascript warts that typescript carries forward for compatibility reasons. But hey, it's the most popular programming language out there - so you'll see plenty of people wanting to write code this way.
The higher order bit is that we both want to bring transpilation after proof tech to mainstream languages.