Comment by auggierose

But yes, this is (partly) a programming language where the uptake will depend on how easy it is to understand.

By the way, I don't have a PhD in mathematics, but I do have a PhD in interactive theorem proving.