2 ms·
For a fantastic intro to the basics and purpose of TLA+, I'd strongly recommend Scott Wlaschin's [1] talk from NDC Oslo this year. Like other academic-seeming s
by jen20 6y ago
For a fantastic intro to the basics and purpose of TLA+, I'd strongly recommend Scott Wlaschin's [1] talk from NDC Oslo this year. Like other academic-seeming subjects, Scott does a great job of applying it to real-world programming.
That said, the answer to your exact question is that it doesn't validate the C++, it validates the algorithm. It's your job to ensure the C++ implements the algorithm as validated!
[1]: https://www.youtube.com/watch?v=tqwcz-Yt9gQ https://www.youtube.com/watch?v=tqwcz-Yt9gQ
- pron 6y agoI wish people use "real" (pretty-printed) TLA+ syntax -- the syntax used when reading a spec -- when giving presentations rather than SANY's LaTeX-like ASCII syntax used to type them. The read/write ratio for maths, including TLA^+ specifications, is higher than for programs, and so there are two concrete syntaxes optimised for those two different modes. I think most people know that on the computer, maths is usually typed differently from how it's read, and they expect to read the maths, not the LaTeX source used to typeset it. It isn't any different for TLA^(+).