You can certainly do readable proofs in Coq the way you would do them in Isabelle, but this requires stating intermediate states explicitly (with assert e.g.) and Coq users rarely do that (mainly because readability is not their goal, I guess).

Or TLA+.

Lamport's structured proofs... should be easier. But I haven't had enough experience to say.