> they include special proof languages that express proofs in a step-by-step way that feels procedural Serious proof developments don't even use the languages

> they include special proof languages that express proofs in a step-by-step way that feels procedural Serious proof developments don't even use the languages in a procedural way. They use "declarative" idioms/patterns that are structured more like a very detailed human proof. This is because "procedural" interaction with the proof state is extremely fragile (it's like raw assembly code, the slightest change in any part of the proof can break basically everything else in it) plus it actually requires "replaying" the proof in order to have any chance of understanding how it works. Declarative idioms can be read and understood directly, at least to some extent.