Suppose you and I are writing a book that develops (classical) mathematics from scratch.
In the course of writing this book, we'll need to define a variety of formal systems, like a system for propositional logic, one for predicate logic; a system for PA, and a system for ZFC.
Now. To carry out all this specification with maximal ease, we should probably settle on a convenient specification language for formal systems, right at the outset.
Question. Suppose we're prioritizing practical usability (as opposed to, say, meta-theoretic simplicity). What would be a good specification language for formal systems?
For instance, I've heard of Post Systems. Would these be a good choice?