Anthony Bordg (Jul 06 2019 at 11:49): Anthony Bordg (Jul 06 2019 at 11:49):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.
Jose Manuel Rodríguez Caballero (Jul 06 2019 at 13:43):Here is a link to a video about Serre's advises (maybe Isabelle is XXI century Bourbaki): Serre
Last updated: Dec 21 2024 at 12:33 UTC