4 ms·

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 wit

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.

JadeNB 1y ago
> 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). Indeed. Lamport says that this was part of what inspired his interest in formal proofs: https://mathoverflow.net/questions/35727/community-experiences-writing-lamports-structured-proofs https://mathoverflow.net/questions/35727/community-experienc....