I'd say if you are starting from a common language, you are already on the wrong path. Doing proofs is so expensive, it is better to optimise your language for

I'd say if you are starting from a common language, you are already on the wrong path. Doing proofs is so expensive, it is better to optimise your language for your proofs, than the other way around.