Subscribe to RCast on iTunes | Google Play | Stitcher
This RCast begins with a discussion of TLA (Temporal Logic of Actions), but most of the conversation focuses on LADL (Logic As a Distributive Law) between Greg Meredith, Isaac DeFrain, and Christian Williams.
Transcript
Greg: We had hoped to talk about the work Pawel had done on TLA. If he doesn’t show, we’ll find another time and talk about some other stuff. TLA is the Temporal Logic of Actions. It’s one of the go-to tools for people who are reasoning about concurrent systems. I would put it as a generation more mature than the Spatial Logic Model Checker. Both are on the same footing, in the sense that you write down a model, and you write down the properties that you want your model to evince (or satisfy), then you run the model checker, and the model checker goes and checks and sees if your model actually supports that.
Pawel was running into some issues in terms of the comms layer that were a little bit tricky for him. So he made up a model; then he made up the properties that he was pretty sure we wanted to support. He was able to find bugs this way, and find relatively quick fixes. Now it’s a decent methodology, but there’s a gap. I wonder if you guys can spot the gap.
Christian: Are you getting at between operational and axiomatic semantics?
Greg: It’s a little bit more down and dirty. The issue is that you might fix it in your model, but then there might be a gap between the model and the running code. You might think that your actual in-production code corresponds to the model, but it might not. So you’ve proven that your model is correct, but you haven’t proven that the code that’s in production is correct. That’s a serious gap. That’s a wing and a prayer.
There’s another methodological issue that I take with these kinds of things. First of all, I want to say it’s an enormous improvement over the methodology where people are just slinging code and testing the hell out of it. It’s basically throwing spaghetti at the wall and seeing what sticks. That isn’t going to work in a concurrency setting. There are just too many ways for the system to go wrong.
Isaac: It’s a lot more useful and believable to prove theorems about your specifications for your code as opposed to if it just passed these tests.
Greg: That’s exactly right. It’s a big improvement, but it’s still problematic in terms of the fidelity of the model to the production code.
Christian: What are the main sources of discrepancy between the program and the model? And why isn’t there some way to ensure fidelity?
Greg: Oh man, you are asking exactly the right questions. The main sources of a discrepancy—and this is what I was trying to get at in terms of the methodological gap—is that the model is typically written in a language that’s very different from the language that people write their production code in. To make this very concrete, if you look at the TLA model and you look at Scala code, they are miles apart. If you look at TLA and Javascript code, they are really miles apart.
This relates to another well known psychological aspect of development. Whenever developers have to face context switches, they lose flow. This is actually quantified. Mihaly Csikszentmihalyi has described the notion of flow. If you go and look at development studies, context switches, places where attention has to shift from one formalism to another or from one tool to another, that’s where mistakes are committed. If you’re going from your model to Javascript or from Javascript to your model, that’s a context switch. That results in a place where errors might be introduced.
From a methodological point of view, we know that there’s a problem. We know that there’s a problem in actuality, in the sense that the code that’s in production is not the model that was checked. We also know that for developers, going back and forth between the two, that’s a context switch. Finally, one of the real issues is that most Scala developers or Javascript developers have no clue, and a lot of them have no interest in, TLA unless they’re really strapped because there’s a serious bug. Then they might go searching for such a tool.
Those are all the challenges that are associated with this kind of approach. I’m not disparaging the approach; I’m simply listing out what are well-known, documented challenges with this approach. How do we bridge the gap? One idea would be to find a modeling language that could be used in production code. The next step would be to have your model checking be equivalent to type checking your production code. This is essentially the proposal with the behavioral types.
That’s why we are interested in LADL in the namespace logic and in LADL in general. Namespace logic for Rholang—which gives us a set of behavioral types, which allow us to express and check a wide range of very impressive properties—fits into the methodology for normal developers. In the case of RChain, where we can nail this down to specifics, Rholang is precisely a production language that can be used as a modeling language in the sense of the modeling language of TLA.
The types that can be derived for Rholang using the namespace logic semantics can be used to express properties like the kinds of properties you can express with TLA. They’re more closely related to the kinds of properties that you can express with the Spatial Logic Model Checker. Spatial logic formulae are very similar to the kinds of types that you can express, but the namespace logic is more expressive because it can see into the structure of names. It can do things that the spatial logic formulae cannot do.
A really good example of this is you can define a notion of a compile-time firewall. At type checking times—this is long before execution—you can assert that a particular process will only communicate on a certain set of names and not communicate on others. In fact, you can unroll this over time. You can have the collection of names (or ports) on your process be open in certain states. Those that are open change in other states and then change yet again. You can define which ports are open at the type level before anything runs. Hence, the term compile-time firewall.
Christian: Has RChain already been using the namespace logic in this way?
Greg: No. The behavioral types come in Venus after we go ahead and get the untyped version of the language defined. Then in Venus, we’ll go ahead and produce the type. In the Rholang 0.1 spec, I wrote down a draft of what the types would look like. It needs some more vetting, in the sense that I wanted to make sure that the syntax for the types feels comfortable to developers.
Syntax is a lot like UI, in the sense that everybody has an opinion on syntax and everybody wants to poke at it. A lot of people poke at syntax with without a lot of experience. It takes a lot of experience to start to get a sense of why a particular syntax hangs together.
I’ve committed most of the mistakes that people make. People come to me and say, “Why didn’t you do this?” Or, “Why didn’t you do that?” It’s like that story about the businessman. “How did you get here?” “Experience.” “Well, how did you get your experience?” “Wrong decisions.” It’s the same story.
We want the syntax of the types to also have the same kind of broad reach (or understandability) for the developers. Probably the version 0.1 of the types syntax will undergo some changes before we roll it out. I want to give it enough time for people to get used to. I was really encouraged because the syntax for TLA properties is very similar to the 0.1 syntax for the Rholang type system that I provided, which is essentially just a syntactic rendering of the namespace logic types.
It was good to see that at least there’s one developer on the RChain team under his own direction. He went off and used a tool that was very similar to the kind of tool that we’re going to provide to the users of RChain. That’s the color and history around the question you’re asking.
I guess Pawel is a no-show today. Next time we can have this discussion with Pawel present because what I would like him to do is to go through some specific examples—a situation where he felt the need to go and get additional support for his development process because he was running into a level of complexity where he needed automated support.
Anyone who’s actually done these kinds of distributed systems, they’ll recognize and feel Pawel’s pain. It is nontrivial. The literature on programming distributed systems and the kinds of errors people make is very much in support that Pawel’s experience is very commonplace, not a one-off. Let me stop there and check in and see if the spiel so far has made sense.
Christian: It’s making sense. Did you say that he essentially implemented TLA with namespace logic?
Greg: No. TLA is an existing tool. He wrote down a model in the TLA modeling language, and then he wrote down some properties in the TLA property language, and then he checked the model. He’s the human mediator between the production code and the model. You need Pawel’s intelligence in order to render that TLA model. That’s the gap that I was talking about.
That’s a really important question that you just asked. This is the gap that we hope to eliminate. What we want is that the code that runs in production is the modeling language. In this case, it’s not the TLA modeling language, it’s Rholang, which is close enough to a process calculus that you can see the process calculus poking through the syntax. You can see how the types would be properties, like the TLA properties or the behavioral types from the Spatial Logic Model Checker or the behavioral types from namespace logic. That’s the idea.
I wanted to go into some fairly deep dive details with Pawel. Part of what’s really fascinating to me about this particular conversation is the difficulty of getting the mathematicians and the developers into the same venue. We’ve been faced with this logistics problem four times now. This is exactly the bridge I’m trying to build: this bridge between the mathematicians and the developers because there’s some really interesting math here.
The namespace logic in and of itself and spatial behavioral objects and the temporal logics of actions, these are all interesting mathematical entities. The LADL algorithm as a generalization of that is also a very interesting area mathematically, but it has really important practical benefits. It’s one of these places where deep, rich, beautiful mathematics has direct application to practical distributed systems. I really would like to broker that conversation between the mathematical community and the developer community, because I think they have a lot to say to each other. It’s very ironic that we’re having so many logistical problems.
Christian: Maybe it’s just different sleep schedules.
Greg: Something like that. We can take the conversation in a different direction. A couple of other topics that I want to talk about from a Brain Candy perspective. One of them is more recent research that’s been going on with respect to LADL, because I’m not sure that the wider audience understands that there are lots of things that we’ve uncovered. We’re finding ways to put this all together into a nice package.
Just to remind people how LADL works: we start with two basic principles. One is something that was uncovered in the thirties. It’s called the Curry-Howard isomorphism. People began to notice that there was this tight correspondence between the types in the simply-type Lambda calculus and the formulae in Intuitionistic Logic.
They were able to give an isomorphism; a translation back and forth. As people dug into this idea, they were able to see that the correspondence was much richer. It wasn’t just that the types corresponded, but that the proofs in Intuitionistic Logic corresponded to the simply-type Lambda calculus terms or the programs in the simple-type Lambda. The correspondence is even tighter. In Intuitionistic Logic, there’s a logical rule called cut, and it’s basically the application of implication to the hypothesis. If you’ve ever been able to prove that A implies B, and you’ve been able to prove that A, then you can apply the implication, A implies B, to the hypothesis, and thereby derive B. This kind of application or cut—all proofs that use these things can be turned into proofs that don’t use those things.
You can get a cut-free proof. The process of deriving a cut-free proof is called cut elimination. It turns out that cut elimination corresponds very precisely to beta reduction in the Lambda calculus. Beta reduction is essentially you’ve got a Lambda term that represents a function that it’s depending on an argument, and if you supply the argument, then you can get the result of the function. That application of the function to the argument is very similar to the application of implication to the hypothesis. The cut-elimination execution engine corresponds precisely to the beta reduction execution engine in the Lambda calculus.
That turned out to be quite interesting. People began to suspect that this way of looking at the world was much, much broader. In the nineties, Abramsky proposed to expand the scope of this. Instead of Lambda calculus terms, you have processes, like processes in the Pi Calculus or other concurrency formulations. The corresponding logics are there. You should get a similar kind of thing, where you’ve got formulae that processes satisfy are equivalent to types that type check those processes. This is the Curry-Howard isomorphism.
On the other side, there’s this notion of realizability. This also has to do with the semantics of proofs. The idea of realizability is that the meaning of formulae should be exactly those computations which satisfy those formulae. We realize the formulae as the terms that satisfy them. Another way to think about it: if you use Curry-Howard, the inhabitants of a particular type—the terms that inhabit a type or satisfy a type—are going to be just those that are the meaning of the formulae.
When you take those two principles into account, then that forces a notion of logical semantics on you. It’s saying that formulae are the collections (whatever your notion of collection is) of terms that evince the particular property that the formula captures. That’s a whole bunch of stuff I just said. Let me stop, take a breather, and check in with Christian and Isaac and see if that makes sense.
Isaac: Yeah, definitely. Thinking about the different formulas that you can have instead of just a collection of whatever objects it is that you’re talking about satisfying those formulas.
Greg: It relates to what developers know in their bones anyway. When you have a really simple type like ent, you expect the inhabitants of that type to be all the integers. If you were to then go a little lower than just ent; if you were to say, “I’m modeling integers as church numerals,” or “I’m modeling integers as Milner numerals or the Conway games,” or whatever, those particular operational intuitions about what arithmetic is, it should be possible to write down a notion of type that would pick out just those computations. You would unfold ent, which gives you no sense of structure, into a type that had more structure, and that structure would force the shape of the computation in a particular way. Then when you collected up all the computations that the structure of their behavior matched your description, that collection should be the meaning of the formula.
As soon as you have that, then you can give a sketch to the semantics of formulae. Typically type constructors are going to be functors. A lot of them, especially if they’re parametric functors, look like monads. If I look at the standard collection gadgets (like set or list or tree) those are all monads. This is where a lot of the category theory starts to creep in. We start to begin to suspect that monadicity captures a fairly decent notion of collection. At this point, it’s just a suspicion. We have to go and check that that is the case for a wide range of notions of collection. Likewise, the whole idea of Lawvere theories allows us to express fairly sophisticated term languages and know that there’s a monad that corresponds to that.
It looks like there’s a monad that corresponds to your term language; the thing that’s going to represent your notion of computation. There’s a monad that represents your notion of collection. Then we know something else, which is that we know that the meaning of all the formulae are going to be collections of terms. It would be the monad of collections applied to the monad of terms (or composed with the monad of terms). That would be the meaning of your formulae.
Now all we have to do is to figure out what the formulae themselves were. We can easily come up with an intuitive note. If you read Abramyks’s paper, “Computational Interpretations of Linear Logic,” and also Abramsky and Vicker’s paper on Quantales and Observational Logic, and also if you look carefully at Caires’s paper on Spatial Behavioral Logics, and if you inform that further with Abramsky’s “Domain Theory in Logical Form,” you began to realize that intuitively formulae are just terms with holes knocked in them.
That makes a lot of sense. How you fill the holes is your collection. It turns out that you can write down a way of combining two monads to give you this terms with holes knocked them, where you’re collecting all of this in terms of your basic collection. That makes a lot of sense. Now your semantics is: combine the two monads, like T plus C, and then it has to go from that combination over to CT. The T plus C can be unfolded into from a language-theoretic perspective, it looks like all the words over T and C.
There’s going to be these funny words where you’ve combined a term and —one word in that unfolding of T plus C is going to be T of C. That’s one of the words that show up in that language. The question is, how would you get from T of C to C of T? If you assume the existence of a distributed law, where you can take a T over C to a C over T, and that’s what the distributed law does, then you can also use the monadic laws to collapse all time where you have a C of a C that just becomes a C with a malt and the T of aT just becomes a T with the multiplication of the monad.
With all of that information, you can canonically construct a semantics. That’s, in essence, the LADL program. The constraints of the principles of realizability and Curry-Howard force our hands with respect to the target of the semantics. They have to be collections of terms. Our intuitions about how we build a term language and how we build collections suggest that they should be monads and that we combine them in a particular way. If we do that combination, we’re forced: the semantics has to go from that combination to the target that we’ve identified. The minimal amount of axioms you have to introduce in order to make that go through canonically is the monadicity plus the distributive law.
That’s the sketch of the argument for LADL. Why LADL is an interesting idea: because if you can push that idea through in a reasonable fashion, then you get a very wide range of applicability. Suddenly you take what seems like the special case of the spatial behavioral logics and the namespace logics and you expand it out to a whole range of programming languages and collections.
There are some interesting things that we’ve discovered along the way. One of them is that the distributive law doesn’t exist. There are these things called no-go theorems. There are certain kinds of monads, like the list monad, will not readily support a distributive law. Set-like notions of collections will support a distributive law. Part of what we’ve discovered over the last several months, where the work is that the kinds of types we’re looking at, the collection part of it is going to be very set-like. It might be a multi-set, so we can probably make multi-set work, or it might be a notion of distribution, like a fuzzy set. We can probably make something like that work. The collection has to be very set-like under certain assumptions about how we build terms and whether or not the monads are essentially tree-like or syntactical in a particular way. I’ve said a whole bunch of stuff there. Let’s see if this is all making sense.
Isaac: When you’re talking about something that is list-like, like the list collection not supporting a distributive law, is it something to do with the fact that it’s an ordered data structure and the set is unordered or is it something along those lines?
Greg: Yes, that’s exactly right. If you grind through the calculations, you need the commutativity of the set. Otherwise, you have one path where you go around one way and you get a particular order of things. You go around the other way and you get a different order. Unless you can equate those two orders, you’re stuck.
Isaac: That makes sense.
Christian: A lot of the no-go theorems were about putting two notions of collection together. In those cases, there were conflicts between certain algebraic properties of the collections. But in general, the term languages will in some ways have less or different structure than collections. For example, in the Rho calculus, the par operator does form a commutative monoid. You need to look out for the similar theorems that talk about a conflict between commutativity and—one of the properties that caused a lot of problems was item potents.
That would be something pretty rare in a term language that we wouldn’t have to worry about as much. Whereas in something like sets, you do have item potents. It’s a very difficult general universal algebra problem given to monads or two theories whether there exists a distributed flow between them. It’s a really interesting problem.
Greg: In terms of this very practical setting where we’re interested in deriving type systems for models of computation. We don’t have to solve the general problem. What we want is a broad enough notion of collection and a reasonably broad notion of computation. That’s still going to be so much better. We need to be able to support things like derive a type system for Scala or derive a type system for Javascript. In those cases, currently those type systems have been developed by hand.
The first versions of the Scala type system were unsound, which is why they had to go back to the drawing board and build Dadi and things like that, which cost the industry a lot of money. Then Javascript had no type system. Now you’ve got the big three—Facebook, Microsoft, and Google—all defining their own versions of type Javascript. Each of those efforts cost tens if not hundreds of millions of dollars (if you do careful accounting). They’re not interoperative. You can’t take darts and deploy it as ECMAScript or so on.
Again, there’s a lot of churn that it creates in the industry. If we get the scope of LADL fairly decent, it doesn’t have to solve the super-hard problems in universal algebra to expand the scope out to where you can just press a button and derive a type system for these kinds of languages, and the type system is automatically sound and complete. That would save lots and lots and lots and lots of money for the industry. That’s why it’s an important endeavor.
There are other reasons to pursue it. That has to do with viewing the type system as a query language. We’re all used to going to Github and treating our code as a kind of data asset. You really can’t search Github on the basis of the structure of the code or the behavior of the code. That makes Github more of a social thing. You have to know somebody who knows somebody in order to find code that does what you want it to do. It could be a lot more effective if we could search Github on the basis of these objective properties about behavior and structure.
You can get a lot of bang for buck in the sense of decent utility without having to solve super-hard problems. I just want people to be aware of that. We’re not necessarily putting fields medal level problems on the critical path, providing good utility for the work that we’re doing.
Christian: In addition to these main capabilities that you want a collection to support, like addressability and membership and that kind of thing, part of one of our main other criteria that will be a more mathematical one is a collection that has the right structure such that many languages distribute over it. Hopefully, that does not imply that the collection has not very much structure.
Greg: Yes, exactly. Again, you don’t have to have a universal collection, although I suspect that set. How many programming languages ultimately have a set data type as part of them? That’s a reasonable approach.
Christian: This is the whole reason I’m in the UK right now. Although I’m not yet answering the question of “What is a collection?,” but more answering the question of “What is a theory?” Marcello Fiori has this really impressive program over the past couple of decades, augmenting the notion of an algebraic theory with a substitution and typing and dependent types and polymorphism and everything that you would want a real algebraic theory of formal languages to have. He’s at a conference right now, but I’ve been studying his papers. It’s definitely what we need in order to have a full algebraic theory of the languages we want to use. It’s really nice mathematics. The conference that he’s at right now, he’s winning the test of time award for the paper abstracts and texts with variable binding.
Greg: It’s a lovely paper.
Christian: It’s very nice. From talking with his students, I’m getting the feeling that he has this very big comprehensive view of this theory of theories. I think that he’s going to be able to provide some very valuable insights about the LADL approach.
Greg: This is awesome. I know that you had mentioned that he has some interest in reflection. If you and Marcello want to sit down over Zoom sometime, we can talk about that. I uncovered this way of thinking about reflection where it relates to integration and differentiation. You have a two-level type decomposition, then you’ve got holes in all your types. That’s the differentiated form. Reflection closes up the hole. That’s the integrated form. You can use those intuitions to derive some nice calculations.
On a completely different topic, since we don’t have Pawel here, we do have a few minutes remaining. I found something really interesting and I want to do a longer session on this, but I just want to toss it out there as a teaser.
In the same way that I was suggesting that reflection has analogies to integration and differentiation, a lot of the standard arithmetic operators have interpretations in the process calculi. In particular, there’s a notion that’s an analog of square root. If I have a process calculus, like the Pi calculus or the Rho calculus, and given a process inside one of these calculi, say P, I can define this square root of P to be the process such that square root of P par square of P is bisimilar to P. It’s a crisp, clear definition.
Then you might ask, “When does the thing exist?” and “When it exists, can I calculate a closed form for it?” Maybe there are some bright people out there that can solve this problem, but I couldn’t calculate a closed form. This has to do with the new operator. But with the Rho calculus, you don’t have a new operator. You can actually calculate a closed form.
I was waiting for my coffee this week writing down a set of equations that we calculate the closed form and I noticed that there was this particular place where something funny happens. When you take the square root of a process that’s of the form P par Q, then you can push it through the par under the assumption that P and Q don’t interact.
Equationally what we’re saying is the square root of P par Q is equal to the square root of P par the square root of Q under the assumption that P and Q don’t interact. If they interact, you have to go and pick out all the tangles—or not. Now, what do I mean by that? You have to find all of the terms that are potentially interacting at a name. That means you’ve got opposite polarities using the name. You’ve got a term that’s sending on the name and a term that’s receiving on the name at a minimum. That’s the smallest tangle. The smallest tangle is red X. But it gets more tangled (or knotted) if you have races. So you could have two outputs on the name and one input, or dually, you could have two inputs and one output. That’s an honest-to-God tangle.
But you could have a lot more. It could be pretty tangled. In order to define the square root, you have to go and pull out all the tangles and treat them separately. What you end up doing when you do this calculation is, again, you’re creating a square root, so you’re going make a copy of the square root of the tangle and another copy of the square root and the tangle. Essentially, you’re going to push the square root through, but you’re going to do it in a funny way where you adapt the namespace.
Now you’ve got two copies of these races, which is a really interesting situation. What if one copy of the race goes one path, but the other copy of the race goes the other path? When you put those in par, they won’t be bisimilar to your original process. They took different paths. To define the square root, you need to force the two copies of these square roots of the races to choose the same winners of the race.
Christian: Isn’t it unnatural to impose some kind of restriction on the future behavior?
Greg: No, it isn’t. In fact, that’s exactly what Casper does. Casper is a protocol that forces the agreement on the winners of all the races. That gives you this really nice equational characterization of consensus in this setting. It’s not going to be consensus possibly in other settings, but at least in this setting, consensus means that you can guarantee that the copies all agree on the winners of the race.
Here’s the really interesting trick. You can go back to this annihilation-style notion of reduction. Let’s just look at the simplest possible red x. We’ve got two sends and one receive. We’ve got two copies of that. There’s some name X. And X is really the quote of a process. To pick out that it’s X as opposed to Y or Zed, we need some component of X to be its identifiers. In other words, P is going to be structurally equivalent. The process P that is that X is the quota is going to be structurally equivalent to some P prime, which is the identity part. The thing that picks out that it’s X versus something else. Then another part that is designed to force the agreement on the winners of the race.
Now you define your comm to happen only when they agree. Because it’s recursive, you’re going to have to keep repeating that at the next level and the next level, until you get down to the origins of your names. You ultimately have to ground out at a set of names over which you can get agreements on these tangles without having to go into any further comm events.
The fact that you’re doing this in this multilayered or recursive style, together with this requirement that you have to agree on the winners of the race, completely pins down the shape of your consensus processes. The square root is forcing a decentralized consensus on two copies. The nth route is going to give you a decentralized consensus on N copies. Is this making sense?
Isaac: The nth route would just be N processes written in parallel that somehow all reduce to this original process?
Greg: When you put them all in parallel, they’re bisimilar to P. This notion of nth route is actually giving you an equational characterization of what consensus means, at least in this setting.
Christian: That’s awesome.
Greg: I wasn’t expecting this at all. I was just pushing the math through. It didn’t occur to me, what is the meaning of this? It’s like some far-fetched analogy from math. What was Ramanujan thinking when he was coming up with these data functions? Who would ever think they would have any sort of applications? Similarly here, I was just following the math. The interpretations leap out at you later.
This is methodologically important. It’s important that we have something like the math even when our intuitions fail, or in anticipation of our intuitions. Then our intuitions catch up and you realize this is actually saying something important. That’s an aspect of having the math and being able to import a perspective.
Christian: That’s an amazing phenomenon of abstract math nowadays: you can take remarkably naive analogies and they ended up saying something quite significant.
Greg: I wholeheartedly agree.