Stream: General

Topic: gold standard


view this post on Zulip 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.

view this post on Zulip 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: Aug 15 2022 at 02:13 UTC