> but since we don't write code like that people can't get to it easily
which likely sums up what Lamport is trying to get across - express your work equationally, determine properties and generally understand what you're dealing with and then later, you can 'compile your equations' down to a particular implementation.
from my own practice, i've found that it is much easier to reason about equations and reflect it down into code than to try and reason about the code
When was the last time you engaged a journeyman carpenter? This problem runs much deeper than just software. Any skilled craft is always at odds with a manager/employer/clients view that you are a fungible asset.
which likely sums up what Lamport is trying to get across - express your work equationally, determine properties and generally understand what you're dealing with and then later, you can 'compile your equations' down to a particular implementation. from my own practice, i've found that it is much easier to reason about equations and reflect it down into code than to try and reason about the code