Hi Andrew,
You seem to be on the right path to learning what formal methods can
and cannot do. You seem to be aware that they are crucial for
avoiding errors in concurrent systems. Are they tedious and
difficult? I think the Amazon experience described by Chris Newcombe
and his former colleagues show that TLA+/PlusCal itself isn't
difficult. Building successful complex systems is difficult, and TLA+
helps make it a little easier. Using any formal language is tedious;
it's easier to write things informally. But a formal language is
necessary for tools, and I find writing in TLA+ or PlusCal to be a lot
less tedious than writing in a programming language because it's a
lot more expressive. But of course, it takes a while to become
sufficiently fluent in a language before that can happen.
The one error I sense in your thinking is a false dichotomy between
formal methods and no methods. It's important to understand what
you're building and, for non-trivial programming tasks, that requires
thinking above the code level. Thinking above the code level means
describing/specifying/modeling what you're doing. You should always
do that. In some cases, you will want to write that
description/specification/model in a formal language. The main reason
for doing that is so you can use tools to check it. Occasionally,
what you're doing is so subtle and hard to understand that it's worth
using a formal language even if you're not using tools. But even if
you don't use a formal language, it's important to write down that
description/spec/model--because that's the only way to be sure you
understand it. Comments in the code are often a good place to write
it. You might want to watch this video:
https://www.youtube.com/watch?v=6QsTfL-uXd8
Good luck,
Leslie