> If the specifications are human legible though, why do you care if the proof (which is checked for you by the machine) is legible? Because it is a goal of an

> If the specifications are human legible though, why do you care if the proof (which is checked for you by the machine) is legible? Because it is a goal of any science not to make a correct model, but also to get a high-level understanding what this model is about. Feel free to call this high-level understanding "what it is really about a "meta-property" of the model, which we also would like to have.