If you structure your code well enough, make judicious choices of names, and fully use the capabilities of Isar, then ideally your code should be almost self-explanatory. Of course, it's an ideal one should strive for, but only an ideal and a difficult one. That's why comments are useful. But, as a benchmark to keep in mind it may be useful .
In mathematics, think of Serre's writings which are seen as a gold standard. Serre somehow embeds a lot of explanations into the structure of his writing, allowing for a great clarity with at the same time a striking economy of means.
Here is a link to a video about Serre's advises (maybe Isabelle is XXI century Bourbaki): Serre
Last updated: Aug 15 2022 at 02:13 UTC