The way it is described (especially the emphasis on how variable substitution is used as the single primitive instead of many different techniques which can tak

The way it is described (especially the emphasis on how variable substitution is used as the single primitive instead of many different techniques which can take years to learn - a phrase which is repeated many times on the website) suggests to me that accessibility to people who would not usually write proofs is a concern of the project. If it is not, the project might not be doing a good job of communicating its goals clearly.