Discussion on: Should Coding be Trivial?

fpuffer profile image
Frank Puffer Author

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

Thread Thread
kspeakman profile image
Kasey Speakman

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.