Pac-man Specification and Synthesis Progress Report 2019-09-29

What happened on this project since the last update in March, 2019, six months ago? For most of that time the project was on the shelf while I worked on other things. But I did manage a few turns of the crank recently and there was some progress from back in April that I never posted, so here for posterity, is a chunk of new stuff.

First, new old stuff! Since this type-driven path-finding synthesis approach feels like it has legs, I spent some time manually sketching out a type graph of "Pac-man universe", which I take to mean roughly the full set of types and functions that would constitute the complete video game. The idea was to discover what the experience of creating that picture was like, as a hypothetical end-user-developer, and what it would be like if the synthesis system of the future would interactively take that and produce the game software as output. Here is the diagram (pdf version).

By my estimation, about 80% of the code in the output game software could be synthesized, with the other 20% representing custom algorithms presumably manually written in the traditional way.

Second, newer new stuff! But first a Pro-Tip™. When putting a project on ice for awhile, it behooves one to leave it in a manicured, clean and stable condition, finishing up intermediate changes, etc. For some reason back in April I did *not* do this, and when I came back to work on the project I found a branch with an unfinished major refactor and a set of mysterious but cool looking mathematical notes scattered in notebooks. It was super painful and difficult to restore the mental context and figure out what I had been planning, and ultimately I had to abandon a bunch of work on the branch, retreating to an older, but stable version. This was very lame. End Pro-Tip™. Anyway, the current new batch of work gets the house back in order, and I've started drafts of a couple math papers that should communicate the underlying ideas both to others and my future self. Here they are: the Flip Machine and the Path Compiler. The recent work embodies the map rule and range rule described in the path compiler paper, although there is yet much debugging to do. This replaces the sketchy prototype implementations that had been previously hacked into place as proof of concept.

Type Drawings. I continue to find it very useful to sketch out type diagrams, as in category theory style arrow diagrams where the objects are types and the arrows are functions. In a software design setting the types would be datatypes and the functions would be program functions (perhaps housed in some process on some machine). But as I have been doing a lot of mathematics lately as grad school ramps up, it's been fun to apply the approach to the proofs I'm writing. My impression is that this sort of approach is similar to what automated proof assistants like Coq must be doing. Example from real analysis (this shouldn't make sense, I just want to show the style):

Future Directions