> 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. Lamp

> 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....