Programs Writing Programs
New Essay
Two workers are quadratically better than one. I shared a first draft of this a couple weeks back; this time it didn't change a whole lot aside from some polishing. But now you can share it with your friends and coworkers if you want.
(While you're at it, I wouldn't mind if you shared the whole newsletter! More readers is good, yay)
Programs Writing Programs
This is my second time writing on PRISM. The first time didn't go so well:
I don't dislike PRISM. It's fun to play with and I like being able to answer dumb probability questions. It's just... what do you even do with it? ... Is it worth learning? I don't think so. It's not going to be useful unless you're absolutely sure you don't need tuples.
I had four major issues with it that limited its usability:
- No collection types, like tuples or arrays
- No string or symbol types (everything is a bool, float, or int)
- No functions with parameters (niladic functions only)
- No "nested" commands as a means of organization.1
These all make it hard to model anything with multiple actors or agents. Each bit of state has to be replicated in a separate variable for each agent, and then the entire top-level code needs to be duplicated. his is all how you get gigantic specs like crowds protocol having to define variables observe0
through observe19
.
In addition to all of the obvious problems, it also means that the most-straightforward way to have multiple agents is to hardcode the logic in. That makes changing the number of agents extra difficult. There are some tricks that simplify this, but that breaks down if we have shared data. If you look at the case study for dining philosophers, they model each philosopher as 12 different states. The shared data, the state of the "forks", is splayed out into all of the philosopher individual states, leading to a mess of a spec.
I used to think this was a PRISM problem, but on investigating other formal methods like mcRL2 I realized I had it backwards. Most specification languages are like this, and I got lucky by starting with TLA+ and Alloy. My guess is it's a focus on tractable specifications vs expressive specifications, and adding collection types and nested transitions makes things harder to analyze.
Still, writing these specs is incredibly tedious and error-prone. And aren't computers supposed to solve exactly that class of problems? I wanted to try writing a program that would write the spec for me. That exercise is actually what motivated the PRISM essay in the first place; all of the queuing analysis was there to justify spec generation.
The implementation was simple. Python has string.Template which can replace $token
identifiers with strings. I wrote most of a PRISM spec template and put a token in the body. Then I could programmatically construct the body as a bunch of computed strings and substitute in the final version into the spec template. This was made easier because PRISM's IDE has "reload spec from file" button, which suggests to me that they intended programmatic generation as a use-case.
The Python file was 900 characters and generated about 1500. This was after I invented a significant simplification to the spec. Before that, the counts were closer to 1000/3000. Importantly, if I wanted to add another worker to the task queue, I can change one number in the Python file vs looking up binary coefficients and writing several hundred more characters of spec.2 I consider this approach successful.
Alternatives
I think there's some potential in using programs to write programs. Here's why I think what I did was appreciably different from other things in the same space:
Compilers
Arguably I'm just writing a compiler (or transpiler as the cool kids call it). I don't think this counts as compiling because I'm not actually doing any lexing, parsing, or analysis. The python script doesn't know anything about PRISM semantics, it's just programmatically building a large text and dropping it in the template.
Source Code generators
Things like Rails scaffolds, yeoman, telosys, etc. Usually used as a starting point: first the generator makes the code, then you modify it to completion. Here we're doing the opposite: manually setting up the code and having the computer complete it. Further, most code generators are black boxes. We control the input but not what it does with the input. Here I want to be able to modify the generator freely.
Macro languages
M4. Designed to programmatically expand text, so potentially appropriate here. I don't know it so can't comment on the differences. It looks like general-purpose computation is possible but very painful.
Template Engines
Probably the closest to what we're doing here. All I'm "doing" is using a template. I think existing engines are oriented towards producing presentation documents like HTML. So maybe more heavyweight than what I'd like here? Or maybe this is where I should be looking. Dunno.
Other issue I see: different relationship between input and template. Most engines may assume the use case of "many reificiations of the same template in different contexts", while that might not be true when trying to write programs.
Other uses
This seems overoptimizing to the specific problem with PRISM: a language hampered by its inexpressiveness. I think there are some cases where programs writing programs could potentially be useful outside of that context. All languages are inexpressive when we talk about possibilities beyond "the code itself". For example, if we want to invasively instrument code for profiling, the instrumentation doesn't have any relevance to the production behavior. We could instead use templates to generate the code with and without instrumentation.
More likely that's pushing it; automatic programming for the sake of spectacle. It might make more sense to explore use cases involving other DSLs. DSLs can sacrifice a lot of expressiveness for the sake of simplicity, so moving expressive complexity to an outside program could be a good idea.
Misc
Maybe I'm just reinventing config files. It's telling that one of the alternative approaches to a probabilistic specification language is JANI, which uses a json schema instead of a lexable language. Easier to read and write programmatically at the cost of human legibility.
-
I didn't talk about this one in the original essay because it's a bit complicated to explain, but you can't have a probability decision lead to another probability decision. Everything has to be top-level. ↩
-
This is a fairly "well-behaved" spec too. If I added certain perturbations, like multiple queues or task priorities, I'd need to write a lot more boilerplate, which would make modifying the number of workers even more difficult. ↩
If you're reading this on the web, you can subscribe here. Updates are once a week. My main website is here.
My new book, Logic for Programmers, is now in early access! Get it here.