I wish the formality would be included in an appendix — as someone who has had to implement a lot of things (and more than once, found errors).
But I agree with your general point: understanding the recipe and general thrust of the approach is often more important, because even if the exact proof misses some technical detail, that can often be patched.
Comments
I wish the formality would be included in an appendix — as someone who has had to implement a lot of things (and more than once, found errors).
But I agree with your general point: understanding the recipe and general thrust of the approach is often more important, because even if the exact proof misses some technical detail, that can often be patched.
Indeed. Lamport says that this was part of what inspired his interest in formal proofs: https://mathoverflow.net/questions/35727/community-experienc....