I didn't hear the talk to get the full context. Do you have a link?
Nowadays, most everyone does (or wants to do) some permutation of Agile. That supports the kind of process you are talking about. (And what I was also referring to.) However, traditional engineering goes through rigorous specification and design (and testing and nowadays simulation). And during some span of time software was approached in that way. And probably safety/security critical software often still is, because the cost of failure is high. So either perspective can make sense depending on the problem domain.
Also bear in mind that Lamport didn't just make programs but helped make Computer Science itself up to this point. So he probably has an engineering background.
It is mainly on TLA+, a formal specification language for concurrent systems that he developed. I didn't mention this in my original post because I don't think that many people (including myself) are familiar with TLA+.
Ah, yes. That is a language for formal verification. Seems like kinda the same principle as TDD, but taken to the level of mathematical proof. You write all the assumptions about the inputs and outputs and side effects of methods. Then you write the implementation. Then the verifier attempts to mathematically prove your program is correct. Yeah, it seems like at that point most of the work would be in defining the assumptions.
For further actions, you may consider blocking this person and/or reporting abuse
We're a place where coders share, stay up-to-date and grow their careers.
I didn't hear the talk to get the full context. Do you have a link?
Nowadays, most everyone does (or wants to do) some permutation of Agile. That supports the kind of process you are talking about. (And what I was also referring to.) However, traditional engineering goes through rigorous specification and design (and testing and nowadays simulation). And during some span of time software was approached in that way. And probably safety/security critical software often still is, because the cost of failure is high. So either perspective can make sense depending on the problem domain.
Also bear in mind that Lamport didn't just make programs but helped make Computer Science itself up to this point. So he probably has an engineering background.
The quote is from this podcast.
It is mainly on TLA+, a formal specification language for concurrent systems that he developed. I didn't mention this in my original post because I don't think that many people (including myself) are familiar with TLA+.
Ah, yes. That is a language for formal verification. Seems like kinda the same principle as TDD, but taken to the level of mathematical proof. You write all the assumptions about the inputs and outputs and side effects of methods. Then you write the implementation. Then the verifier attempts to mathematically prove your program is correct. Yeah, it seems like at that point most of the work would be in defining the assumptions.