Feedback Mikhail

[kappelmann]

Here is some feedback I received by e-mail by Mikhail:

1. Overall, it would be useful to have standardized style guidelines both for the AFP and Isabelle-dev. If these guidelines can be enforced through automation, better yet.
2. "Files should not be longer than 1500 lines...". I agree that there should be a suggested limit on the size, but 1500 seems too short. There are many files in the standard library that are substantially longer. For example, Topological_Spaces is nearly 4000 lines long. Personally, I try to ensure that my theories are not longer than 3000 lines with the hard limit set at 5000 lines.
3. "Undocumented ML-code - or code in general - is virtually incomprehensible." Is this a fact? :-) I believe that I have read somewhere that "ML-code is self-documenting". Personally, over the years, I converged on the opinion that comments in any code are detrimental nearly always: they create a maintenance burden and are easy to forget about when making changes to the code. However, this is a matter of taste and opinion. Nonetheless, to me, the sentence itself looks like it is a part of some kind of complaint, not a part of coding guidelines :-).
4. The 0th chapter of "The Isabelle/Isar Implementation" contains quite a number of style guidelines for the Isabelle/ML programming. My personal opinion is that the ML-part of the guidelines should merely reference the aforementioned document. Alternatively, it may be plausible to merely copy all matters concerned with style from "The Isabelle/Isar Implementation".
5. There are many valid points raised in https://proofcraft.org/blog/isabelle-style.html. However, I am not entirely confident if all of these are covered in the new proposed style guide. Perhaps, it would be sensible to cross-check these documents, unless, of course, it has already been done.

[kappelmann]

1. Overall, it would be useful to have standardized style guidelines both for the AFP and Isabelle-dev. If these guidelines can be enforced through automation, better yet.

I think that's true but lies in the distant future. The rules must first by tried in practice in smaller (e.g. student projects).

2. "Files should not be longer than 1500 lines...". I agree that there should be a suggested limit on the size, but 1500 seems too short. There are many files in the standard library that are substantially longer. For example, Topological_Spaces is nearly 4000 lines long. Personally, I try to ensure that my theories are not longer than 3000 lines with the hard limit set at 5000 lines.

We got similar feedback before, but as said, it is not a hard limit. I do personally believe though that files with 1500+ lines of proofs can be split up in a sensible way in most cases.

3. "Undocumented ML-code - or code in general - is virtually incomprehensible." Is this a fact? :-) I believe that I have read somewhere that "ML-code is self-documenting". Personally, over the years, I converged on the opinion that comments in any code are detrimental nearly always: they create a maintenance burden and are easy to forget about when making changes to the code. However, this is a matter of taste and opinion. Nonetheless, to me, the sentence itself looks like it is a part of some kind of complaint, not a part of coding guidelines :-).

I agree, that phrasing is very opinionated and unprofessional. I removed it in c74f93c1a3fccb62e6995928857a55aa51669ad2

4. The 0th chapter of "The Isabelle/Isar Implementation" contains quite a number of style guidelines for the Isabelle/ML programming. My personal opinion is that the ML-part of the guidelines should merely reference the aforementioned document. Alternatively, it may be plausible to merely copy all matters concerned with style from "The Isabelle/Isar Implementation".

This is a good point. I will add it to the ML documentation thread.

5. There are many valid points raised in https://proofcraft.org/blog/isabelle-style.html. However, I am not entirely confident if all of these are covered in the new proposed style guide. Perhaps, it would be sensible to cross-check these documents, unless, of course, it has already been done.

We are in contact with Gerwin and will see if we can reasonable align both guides. Gerwin already told us that he is keen on doing so.

[kappelmann]

Very much appreciated feedback. Please drop any further comments as you wish.

[lukasstevens]

We should reference the guide by Gerwin. But we consciously kept most of it out of this guide since Gerwin's guide is more about proof engineering which is not the focus of this guide.

[lukasstevens]

I still think that ML-code should be documented. There are several instances when the code as documentation is not really enough: if there are some implicit assumptions on the arguments that don't get checked, if the code combines several other functions in a non-trivial way etc. Sure, keeping the documentation up to date incurs some work but I think it is worth it.

Of course, if the name of the function already tells the whole story, then you don't need a comment. Good comments explain the how and the why, not the what.

[kappelmann]

I still think that ML-code should be documented. There are several instances when the code as documentation is not really enough: if there are some implicit assumptions on the arguments that don't get checked, if the code combines several other functions in a non-trivial way etc. Sure, keeping the documentation up to date incurs some work but I think it is worth it.

Of course, if the name of the function already tells the whole story, then you don't need a comment. Good comments explain the how and the why, not the what.

I do agree - do you mind posting this to the relevant ML documentation issue? #7 Thank you

[jaycech3n]

if there are some implicit assumptions on the arguments that don't get checked

Especially, and more generally, the invariants that the code is assumed to maintatin. Multiple threads on the mailing list have raised such issues in the past.

[lukasstevens]

In general, it should be documented which assumptions the code makes about its inputs and which assumptions can be made about the output.