> no general purpose programming language lets you put an arbitrary expression in the same language in a type as a permanent condition, or lets you state facts that the compiler will prove

Lean can be used as a regular programming language. There's also languages like idris2 and f-star, but they don't seem to have much traction.