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