I found this elaboration and clarification very illuminating. Thanks!
This makes a lot of sense, and is quite cool. I think this is the kind of thing I have in mind for ways of getting mutually beneficial exchange from the model checking and theorem proving approaches. I think I finally, properly understand your point about the modeling and proving using TLA+, and how that is separate from the use of model checking in this context. Thank you for explaining.
To clarify regarding
I didn’t mean to suggest you were saying this. That question on my part was meant to go back to the general question of this post, but I didn’t signal that very well. I think your remark here helps to clarify (for me) what is going:
I guess part of the difficulty (for me) in fully appreciating (or accepting) this perspective as it pertains to programming languages must come from the fact that in the propositions-as-types approach, we also have language-level constructs to describe systems, and reasoning about the programs in the language is the way we reason about the system so described. I do think I understand and accept your point, tho, that the special-purpose design of TLA+ (and it’s ability to ignore any concerns of maintaining isomorphism (not to mention identification) with programs) has enabled it to be very expressive and concise, and obviously used to good effect.
Again, very interesting for me to read your reflections here, @grayswandyr. Thank you 