I think that converting C to TLA+ is too low level; TLA's state space would explode before anything of consequence can be explored. There have been similar academic efforts to convert from SPIN's Promela to C, but nothing interesting has been shown.
So, we have TLA+ on the one hand, which is too abstract, and C on the other, which is useless when translated to TLA. I think that a better solution is to have a DSL tailored to the domain, which can generate C for performance as well as a TLA+ model. Anil Madhavapeddy's PhD dissertation is a good example:
https://www.cl.cam.ac.uk/techreports/UCAM-CL-TR-775.html
> TLA's state space would explode before anything of consequence can be explored
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.
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.
> I have not really been able to get anything beyond the most trivial to work with TLC, so I just stick to TLA+.
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.
So, we have TLA+ on the one hand, which is too abstract, and C on the other, which is useless when translated to TLA. I think that a better solution is to have a DSL tailored to the domain, which can generate C for performance as well as a TLA+ model. Anil Madhavapeddy's PhD dissertation is a good example: https://www.cl.cam.ac.uk/techreports/UCAM-CL-TR-775.html