RChain developer Pawel Szulc leads a discussion on TLA (Temporal Logic of Actions) with Greg Meredith, Isaac DeFrain, and Christian Williams.
Greg: It’s been difficult to get everyone in the same venue, partly because of time zone issues. As I mentioned the last time we were attempting this, I feel it’s representative of something that happens culturally. It’s really hard to get the theorists in the room with the practitioners; it’s also hard to get the practitioners in the room with the theorists. However, when it comes to grant-writing time, the theorists really need to justify their work in terms of the practitioners; when it comes to shipping and sweating bullets about the correctness of their code, the practitioners really want the assurance from the theorists that things are going to work out.
We’re at that point where the rubber meets the road. Pawel, what we had ultimately wanted to talk about was your experience with temporal logic of actions, TLA+: what drove you to use it, what your experience was, and then talk about that experience in the context of what we ultimately want to deliver with the behavioral type system for Rholang.
Pawel: Let me tell you my story, which has been a fun experience with formal methods. I had absolutely no idea what formal methods were a year ago. I’ve been using them for some dependent type languages, but the term itself was completely new to me. Then I stumbled upon a presentation at one of the conferences in London two years ago. That presentation was prepared by Kathleen Fisher. She was talking about this program called HACMS. This was a DARPA program where they performed research on whether formal methods can eliminate an ...
To keep reading, please go to the original article at:
RChain Cooperative - Medium