Wide adoption of TLA+? Terry Coatta update on my chat with Leslie Lamport, ACM Turing Award winner in 2014 (for 2015 now 1 million USD prize for Nobel Prize of Computing)
I had a conversation with esteemed developer Terry Coatta on TLA+, which Leslie Lamport, ACM Turing Award winner in 2014, talked about in my chat with him.
Terry says: As for TLA+, I suspect that it will receive similar treatment to many of the formal approaches/tools that have been developed. That is, I think there are some folks who will be able to apply it, but I doubt that it will see broad adoption. There are a couple of reasons that come to mind.
First, many development teams are not directly building distributed infrastructure themselves. Instead, they rely on infrastructure developed by others. So, for example, many applications use Redis for distributed caching. This relieves them of the need to create such an infrastructure themselves and reduces their need for sophisticated analysis tools.
Second, ‘real’ applications tend to have a bewildering variety of edge cases due to complex customer driven requirements. My experience is that these formalisms work well for small, constrained problems, but are unwieldy for the more ‘sprawling’ sorts of applications that we find ourselves building. Teams building focused infrastructure pieces are probably in a better position to take advantage of these tools. So, I could more easily imagine the folks who build Redis using TLA+, than I could my own team.
For more on Terry, see: https://blogs.technet.com/b/cdnitmanagers/archive/2014/11/04/register-for-december-3-webcast-quot-data-access-and-entity-framework-quot.aspx