You are clearly engaging in bad faith at this point when you pick the "car not being useful for everything" analogy and you cherrypick it into absurdity. For so

You are clearly engaging in bad faith at this point when you pick the "car not being useful for everything" analogy and you cherrypick it into absurdity. For someone that says is interested in distributed algorithms it's clear you are not interested in being able to reason, about them. EDIT: There was an edit adding the final part of the comment after I submitted mine above. Here is my response to the last part, since the comment was toned down a bit: Yes, we need to improve the tooling, and TLA+ can be improved a lot, I'd love for it to be able to reason about my code and to have an easier bridge between both words. However engaging in the discussion of how it can be improved without acknowledging what good and usefulness it brings is just not useful in general, and it just puts off people that could benefit from it from ever using it. TLA+ has a lot of value in some cases, and we should be acknowledging that!