True that. I have not really been able to get anything beyond the most trivial to work with TLC, so I just stick to TLA+.
> TLA+ is not "too abstract". It is mathematics.
I understand. I'd wager that is the chief reason why most programmers don't even begin to investigate it. Spin feels easier because it is operational and because it can incorporate C.
Really? I personally have checked quite elaborate TLA+ specifications with TLC, and I know others have, too. Sure, like all verification tools it's got its limits, but even for a complex distributed system spec, TLC could reasonably check it with, say, four nodes.
> I'd wager that is the chief reason why most programmers don't even begin to investigate it.
I'm not sure Spin is used more than TLA+ these days, especially when it comes to "mainstream" software.
You're confusing TLC with TLA+. TLC will work for small programs, but you can still use the TLA+ proof assistant (TLAPS) just as you can use Coq (and for the same definition of "can").
> So, we have TLA+ on the one hand, which is too abstract, and C on the other, which is useless when translated to TLA.
TLA+ is not "too abstract". It is mathematics. It can describe a system at the level of general algorithms, or at the level of logic gates. In fact, it particularly excels at expressing abstraction/refinement relationships between descriptions of the same system at various levels. For example, you can establish a refinement from the C code to a higher-level spec with the proof assistant, and then use TLC to model-check the higher-level spec. But still, TLA+ is not likely to be any better than Coq, or any other deep specification and verification tool. Unfortunately, none of them can feasibly verify software of common size.