DEV Community: Marianne

Programs Split Over Multiple Files (featuring Troels Henriksen)

Marianne — Wed, 14 Apr 2021 04:37:23 +0000

Summary

When thinking about how to create a language where little models can be combined into bigger more complex system models, Marianne struggles to understand why not to take the completely straight forward approach of importing files. While searching for a good explanation she comes across the official blog of Futhark and decides to interview its lead on their design decisions.

Links

Design Decisions I Do Not Regret

r/ProgrammingLanguages

Fault-lang WIP Compiler

Bonus Content

Become a patron to support this project.

Transcript

MB: Back when I started this series, Thorston Ball made a comment that stuck with me

MB: Is there something that you would really like to see people like add to Monkey that hasn't happened yet?

TB: I would be interested to see, like, a really well thought out module system.

MB: And I thought to myself …. what, is that hard? Oh crap…. that’s probably really hard isn’t it?

TB: And I feel like that is…. I don't even know what that means, you know?

MB: I added this to my research list—figure out module systems—and surfed over to my favorite community for program language design advice: r/programminglanguages. This subreddit is full of great stories and people will give detailed explanations and encouragement, which is rare on the internet these days.

MB: While reading through conversations on r/programminglanguages I came across a blog post on the official site for this niche functional programming language called Futhark. Futhark is an experimental programming language for high performance computing run by the University of Copenhagen. Because of that, their blog is full of interesting design discussions, including a post entitled Design Decisions I Do Not Regret which— among other things—goes into the design of Futhark’s module system

MB: So I asked the author of this post, Troels Henriksen, to chat with me about why he created a programming language and how he thinks about these decisions.

TH: I think one of the problems was that when you are a bank every day, you must you must figure out how much money you have. And in a modern bank, it's not just about counting how much money you have in your vault. It's about counting how much your various contracts and options and derivatives are worth. And often there is no easy answer to that because that's actually a probability distribution, because if you have an option that allows you in two weeks to buy some stock at some price, then the value of that option depends on what that stock may be worth in two weeks.

MB: Yeah

TH: And that's and you have to figure that out. You basically have to a Monte Carlo simulation to figure out what to look at. What are the various ways the stock market can go and then take the average or something? I don't fully understand all the mathematics behind it.

MB: (laughs)

TH: Yeah, and imagine if you had to do that when you're looking at a banknote…. But that means that when you want to price options, you need to be able to do a lot of compensation very quickly. Yes, you have one day to figure out how much it's worth and it's kind of obsolete information. So there was interest in doing High-Performance functional programming. And and that was kind of as much of a plan as there were. And then I got involved as I was a TA n a compilers course in my department. And one of the teachers was involved in this project. And he recruited students to try and work on a language that was supposed to be for GPU programming in a functional style. And I’d been a TA in the course, and I I didn't like the way he had designed the compiler. And so I wanted to show him a better way of doing it. So I took his very early draft of a syntax tree and rewrote it and made it better. And then I just kind of went on from there in my free time and created a very small compiler, generate sequential code, wasn't very fancy. And then he hired me as a student programmer and eventually as a Ph.D. student.

MB: But like what kind of— what is the average user use it for, like, did it end up being used in the use case she thought it was going to be used for like banks…?

TH: I don't think there are any actual banks that use it because that's also not really— we need to really expect that banks are conservative and it's a research project. It's not supposed to be a product. But Futhark was kind of by accident, designed to be really good at Monte Carlo simulations. And it is still useful that to some people. But I would say the average user of that is either a student who has been forced to use it for a project—

MB: (laughs)

TH: …or an independent researcher who is trying to investigate some new kind of model where, sure, they could write up in Haskell, but then they would not be able to validate their model because it would run too slow. And the model is too unusual to easily express in TensorFlow or raw primitives like GPU, linear algebra functions. So Futhark is a nice compromise where you have a lot of flexibility to just change things and try things out, but it still runs pretty fast on GPUs or multicore CPUs and so on.

MB: So how do you approach making design decisions for the language that you're working on now or like languages you worked on the past? You mentioned that the the original spec had a compiler design that you didn't think was all that efficient. Right? So you chose a different design, like how do you approach that decision making process?

TH: So Futhark has actually changed a bit in superficial terms a lot since it started. It started out being a very crude first order language that kind of resembled Standard ML a little bit, but it had parentheses for application and so on. It was kind of nasty. Was designed by my former advisor, who is an excellent compiler engineer. But his previous life was writing Fortran compilers in C++.

MB: Nice!!!

TH: We disagree on certain points. So gradually the language became what it is now, which is more Haskell like more classically lambda calculus style and usually the way since we don't to try to innovate that much in languages, we want to just use the language a little bit. And then we said, well, this sucks, this looks really ugly, can we do better? And we just looked at mainstream languages and of course Haskell is mainstream that and we figured we just what can we do better? Inspired by these language.

TH: So we didn't actually innovate a lot, which was just copied from other languages. And I think that's actually a good way of designing a language because they're the design space is enormous and the vast majority of of design decisions are terrible. I have terrible interactions with all those design decisions. So innovating actually doing something completely novel is really dangerous unless the novelty is exactly what you're going for.

MB: Yeah

TH: Something like the syntax and the type system and so on. That wasn't really what we were trying to innovate on, at least not initially. So we just looked around for things that people only tried and used for decades and we knew what worked and what didn't. And then we were talking maybe a little bit because existing languages have things that that that have some flaws because they weren't realized initially. And they can change it because backwards compatibility, but then we can tweak them a little bit. But we intentionally tried not to to innovate too much in areas outside of our core competency.

MB: I’ve heard some variation on this advice from several people so far: pick something you like in another language and copy the implementation to start because figuring out all the edge cases from scratch is really hard. And for the most part it has been advice that I have followed.

MB: But the problem with module systems is that even after reading a bunch of arguments about it … it just …. seems easy? Right? Like I’m sure if you want to do something with object inheritance and complex namespaces it’s harder, but at the end of the day isn’t it just importing code from another file into your program? I know the complications must be there, but I can’t really see them for myself.

MB: The debate comes down to this: you can do imports using file paths strings— maybe just the filename if the main file and the code being imported are in the same directory, or a relative path using dots and slashes to define where in the file system tree the code to import lives.

MB: Or you could do something more sophisticated where the module location is defined relative to something other than the file where the import is taking place, perhaps the application root directory.

MB: Obviously most mature general purpose programming languages use the second approach, but I would prefer the simplicity of the first approach to be honest…

MB: From my vantage point, being able to split a system specification into smaller parts means you get to reuse those parts and build progressively more complex systems that are in easily digestible chunks. So I've been trying to figure out exactly what is the lay of the land on on this and like how—where are the complications? And that's how I came across the stuff that you had been writing about your own journey through this, which I found really easy to read and compelling, which you do not necessarily find to be the case about programming, language design writing. So I'm interested in hearing more about how you came to the decision you did and like why people look at that more simple file import pattern and go, oh, no, but when you get to larger programs, that's a disaster. So don't do that.

TH: Yes, so, perhaps we should clarify what you mean by module system, because it's actually two distinct things here. One is modules as a thing that allows us to separate a program into multiple files, which, of course, both desirable and probably also necessary. And then there is an orthogonal concept, which is about how you can structure your program in terms of namespaces and also more advanced modular features, but namespace probably what most people associate with modular systems. Yes, these are all orthogonal.

MB: Yeah so… Quick question. Is there an actual specific term for one versus the other or is it literally that is the same term? Because I've had this conversation multiple times where I'm like, “How do I build a module system?” And everyone is like: “Well, what do you mean by module system?”

TH: Yes, no, I have actually been thinking about that ever since you invited me to this interview. And unfortunately, there is no term for splitting things into files, at least not academically.

MB: OK, good.

TH: I think it's because the academics consider it as a boring problem or haven't discovered why it might be interesting. So in an ML they call it, they have something called the basis system which does this. But it's I think that's a very ML specific term. And I would say it's not one of the most successful parts of the design. So let's ignore that. But I think it's because you can always take a program written within multiple files and then just concatenate them and pretend them that it was a program all along.

MB: True.

TH: Of course, it's not practical, but. But that's a separate thing.

TH: OK, but so are these two things. And then of course, related in most languages and in many languages. You only have file division. That is also the unit of modules. And I think Java ,Java is complicated because you have the split into files, which I think is called packages in Java. But then classes in Java also behave a lot like modules because each encapsulate a namespace that prevent them from clashing and they can they do access control on a name. So that's a bit like like modules. So. in Futhark, what we have is, of course, ML style modular system. It's taken almost verbatim from standard ML, but with some places a few extensions… in particular, a syntax improvement. And that is a very odd modular system. So ML doesn't talk about files at all. So the module system is built with the assumption that your program is just one big file.

MB: Mm hmm.

TH: And then the module system can do the usual stuff, you can you can create a module and you can have definition inside of that module, and then whenever you want to access one of those definitions, you have to prefix them with the module name, just as usual name spacing thing that you have in any other language. But then ML also adds extra signatures, which allows you to say, I have this module and this module implements this signature, and then you can only access those parts of the module that are defined in the signature that allows you to hide names and make types abstract. So that's how it's information holding

MB: Like Public, private. And you have to export it essentially.

TH: Yeah. Yeah. Oh, yes. Yeah, kind of. Except that it's kind of separated from the module. Modules and signatures are separate and you can have multiple modules and implement the same signature. So it's kind of like interfaces and classes. But but you can instantiate emotion. It doesn't make any sense. It's also a little bit like header files in C and files, of course. And C is a mess for other reasons.

TH: But then ML goes even further and they add this notion of functor or parametric modules, which is kind of like a function at the module level where you can say if you give me a module that implements the signature, then I will give you back a module that implements other signature. So, for example, if you give me a module that implements a signature for numbers, then I will give you back a module that implements various linear algebra operations on arrays that contain that kind of numbers. So that's kind of a way of doing genetic programming at the margin level that that ML pioneered in the 70s and 80s, and that is is an aspect of ML that hasn't really been imitated in many other places because it is kind of a complicated system and many other languages to this with type classes or traits instead.

MB: So what are the what are these kind of constructs prevent? Because like so if we we have a module system that just concat needs multiple files together and treats it like that, that's very easy for me to understand why that could potentially go wrong. You have namespace issues like right off the bat. Right. But you could like sort of create a map that broke down in namespaces into scope's really easily and then like do that. And that seems to me to be like not a super hard thing to do. So why do this? The why does it seem to have more complexity than that? Or do we just refer to it with fancy terms that make it sound like it has more complexity than that? But ultimately, that's all that's going on?

TH: No, I mean, the main reason why we like this idea of splitting things into files is, is to enable separate compilation. But thing I think it's easier to solve technically, you can just take everything with a unique identifier and then with make symbol tables, you can handle that easily enough. But a separate compilation is, of course, critical for any large program. You don't actually want to recompile everything all the time. And files are a very natural notion of very natural unit of splitting up into. So every source file becomes an object file or a class file or whatever. And then only when you change the source file, you have to change the object file regenerated object by combining them all at the end to get your program that works. And and I think almost all languages work that way, even if they're not, if they are trying to hide it.

TH: So this idea of just concatenating all the files, that there are two ways of doing it in the style of doing it. In the ML style of doing it. Sure. Conceptually you can naming all of the files, but they still all individually type check and parse check and all this on their own before the compiler starts putting them together and then doing co-generation or whatnot. Whereas in C, this concatenation of files really is just inserting the contents of the header file or whatever else, and you can include anything you want. Doesn't have to be a header file. And just putting it in way they include was if through the same file multiple times and you get multiple copies of the file, take precautions to avoid that with practice or or the if-not-def trick that is ever present in C code. And then only after that inclusion has been done by the C parser get to run. So you can kind of have files that look syntactically incorrect. But then after all the inclusion is done, they are suddenly typed and the syntax is correct.

MB: Okay that made sense: separate compilation, and figuring out when the parsing and type checking happens. I’m beginning to feel more comfortable with this now.

MB: I hate working in languages that have confusing import paths schemes like this is my number one biggest, I am annoyed by the way you do this in this language, like first… learning-a-new-language-thing is not being able to figure out, like knowing where the file is on the computer and not being able to figure out how to get it to import things correctly.

MB: So, like my gut instinct is here is to just make it so that people can go like …/ ../ Here's where my file is like, please import this file right like that. That to me is the easiest and most intuitive thing. And the feedback I keep getting in this very cryptic fashion is. “But if you do that, people can't write large programs easily.” And for the life of me, I do not understand why people believe that to be the case. Like why would make a difference? Right. I feel like it's just an interface versus like… I don't know why I get that feedback. So I was interested in your perspective, having also made a decision, from my understanding, to go in the dot-dot-slash versus just using import paths.

TH: Well, I agree with your initial analysis. I think no one enjoys learning about import behavior. So when we initially improve the design, the file includes mechanism. And again, that's was one of those things where we really had no ambition to improve on the state of the art. This was not our research problem. We just needed some things we have two files in one program. And so we looked at various ways of doing it. And initially we did something python like where you write the name as kind of a variable name and with dots, and then that gets translated into a file name by some builtin rules. And eventually we just look at it and said, why isn't this just a string literal giving the filename? It is a file at the end are we trying to hide it? And that languages or have been languages that run in more advanced settings where we don't have files, IP image based system like Smalltalk or lisp machines or or unison for a much newer example that are trying to innovate and say, well, what if we didn't have files in our language, then that's cool. And I think it's very worthwhile research. But unless that's what you are doing, don't hide the files. I mean, there are files that people are going to be frustrated that they can't just access them. And then, of course, maybe in 10 years when we are all running on the unison VM, maybe I'll come up with another syntax so you can import some object storage based on the content based hashing or whatever. But for now, files are fine.

MB: Yeah.

TH: So the reason why I think some people suspected some scale is that if you are an extremist about it like I am: in Futhark the file name is relative to the important file.

TH: So that means when you move files around, you may have to change the import strings to reflect where the files are now located relative to the important file. And I guess people will think that will be too much of a bother. Well, first, I think it's pretty easy to automate because that is just you can you can you can find quick scripts to fix this just based on your understanding of hierarchical file systems, which are pretty universally understood by every programmer. And second, if you will, if you really have tons of imports every file, like dozens, but you might in a real world system, Futhark is for small programs. So we don't have that. But I can see that might happen then. I think you can address that if as long as you have a nice mechanism for re-exporting multiple files from one file, like what we call them open imports. So that's and I guess all the language might have other names for them. And if you can do that, then you can just have one file that includes that in some some single known location that includes a bunch of other files based on that location. And that's the single file that that is included by all the others. And that means you have less to update when you when you move stuff around.

TH” But I don't know if it's really that common to constantly just move files around. And if I include statements all the time, I I've never worked on truly enormous systems. So I don't know, maybe I'm just talking out of ignorance. Yeah. But I can't believe it's that big of a problem.

MB: I mean, like I think it might. I also don't know how often people just move stuff around. Like I spend a lot of time professionally working on the maintenance of old systems and generally speaking, getting anybody to do any kind of re-architecting or redoing of code that's already on a file somewhere. It's just pulling teeth. So I have a hard time believing that people just arbitrarily moved, rearranged their files on a regular basis. But I also am not sure that you don't end up in the same problem when you're using a more complicated, like import part syntax and also moving. I'm not sure it's clear to me that that that problem is not also a problem when when you have a more complicated import file import scheme.

TH: Another reason that people think it might not scale is because of what it looks like. So when you design a language, you kind of you probably use in designing a language that is better than some specific problem. And probably you are to some extent motivated to designing a language that looks a lot like the languages that are already solving roughly that problem. Of course, you will try to do it better. And if you think about languages that use filenames to import all the files and then use less language like PHP and Shell scripts and to the extent C where it is also a little bit messy, whereas languages that we acknowledge are more well designed like Java or Haskell, they use some more abstract notion. They use package names or module names which are translated to files eventually with some mechanism. But but they don't just put a string that there. So you end up thinking that, well designed languages, they don't refer to files. But I don't think the problem with PHP is that

MB: (laughs) It's certainly not the largest problem with PHP.

TH: The problem with PHP and Shell script is that when you include all files, sure, you can put a string literal to there, but you can also put a piece of code in your computer file, including and that's, of course, madness. And then you cannot analyze it statically. But in Futhark, you put a string literal in the import statement, and that is technically a literal it cannot be an expression. So it might look like it's the same thing as in PHP, but it isn't. That’s full static knowledge. nothing fancy going on. You cannot do a dynamic import or anything like that.

MB: So…. this is going to be the last episode for a while. I’ve made some design decisions I feel really good about, but it’s clear that the only way to validate them is to write code and try things out. I’ll be back in a couple of months to let you know how that went and do some research into optimizing the compiler. But I really just need to just be heads down hands on a keyboard for a while on this.

MB: If you want to track my progress, maybe send me a pull request to correct all my stupid mistakes. I’m pushing code to a repo under the Github Org named Fault-lang. If you’d prefer a less intimidating way to participate in the development of my fledgling language, I got one additional great piece of advice from Professor Henriksen:

TH: Oh, and another piece of advice, find a cute animal mascot for your language.

MB: I know! I've been really thinking about that, thinking very hard about that.

TH: I have my Futhark cup here that one of the PHD students did.

MB: Is it….?

TH: With a hedgehog

MB: Oh, it's a hedgehog! I was like I first thought it was a monkey. And then I was like, no, it looks like hedgehog… It is a hedgehog?

TH: Yes.

MB: Ah cute! Yeah, I know. I have to figure out what our cute animal mascot is going to be because that's really… that's really critical to a language’s success or failure is the ability to have an attractive logo and a cute mascot.

Code Generation (featuring Tikhon Jelvis)

Marianne — Wed, 07 Apr 2021 12:45:43 +0000

Summary

Part of Marianne’s flash of inspiration came from a talk she’d seen about translating programs to a form Z3, a popular SMT solver, can run as proofs. Full of enthusiasm she invites the software engineer who gave that talk, Tikhon Jelvis, to elaborate on the similarities between SMT and code normally generated by the compiler.

Links

Compose 2016 Analyzing Programs with Z3

Tikhon Jelvis’s Website

Jelvis’s Foundations of Reinforcement Learning

Z3 tutorial

Bonus Content

Become a patron to support this project.

Transcript

MB: Sometimes when I think I’ve had a really great idea it blows everything else out of my mind. I love this feeling. Especially when facts I thought were unconnected click into place and filled out a whole bunch of context I had been missing before.

MB: In my experience this is the reality of learning new things. It’s not a steady stream of knowledge being inputed into my brain. It comes in flashes that interrupt these long dry periods where I’m hearing words and translating them into meaningful sentences but the concepts themselves are not meaningful.

MB: This came up in my conversation with Ron Garcia actually

RG: I've said this a lot to people that at some point I started just going to things I didn't understand and I just sort of let it wash over me and like, I have no idea what's happening, but I'm just going to pay attention. And then I leave and I'm like, it sure doesn't feel like I learned anything, but something happened. And then and then, like, you go back again and then one day you're just like, wait, I know what that means. Or you ask a question and they're like, oh, good question.

MB: Yeah.

RG: So you're doing something.

MB: You have a moment like Neo in the Matrix. A sort of “I know. Kung Fu” moment.

RG: Yeah, exactly.

MB: It comes out of nowhere nut it's actually like years of exposure to things

RG: Totally. Like who put that there?

MB: Exactly.

MB: So when it occurred to me that the best way to implement a system modeling language that can use probability might be to use formal logic of a traditional model checker to bypass the need to run simulations, I immediately thought of a talk on SMT solvers I had seen on youtube a few months before. Tikhon Jelvis gave this amazing talk at Compose in 2016 called Analyzing Programs with Z3 that was the first time I had seen someone use SMT formulas to actually model stuff that is relevant to programming.

MB: Typical example models most experts use to help people learn are games: solve a sudoku, here’s the eight queens problem, the famous Zebra word puzzle… things like that. So when you start learning this kind of tooling the learning curve isn’t just steep. It’s got this bottomless crevasse in the middle where you have to somehow make a jump from Highlights puzzles to pragmatic programming without any references.

MB: I loved this talk the first time I watched it and then as I rewatched it I realized that the steps of converting a piece of code into a representation that can be modeled in SMT were the same steps I was working through in different tutorials on writing compilers.

TJ: So to convert to a formula, there are basically three steps, the first one is in-lining all our functions now. I mean, I didn't talk about functions here. And the main reason is because after we in-line them, we can just pretend we didn't have any. Then we unroll all our loops and we transform it into something which is single static assignment style. I'll go into what that means in the next slide, but so in-lining. Again, if we have functions, basically all we do is we create fresh names and then paste function body into where it was called.

TJ: So this is sort of how the CPU process works, except I think it didn't even create fresh names. The biggest advantage of in-lining, of course, is that our formula doesn't have to know anything about functions. We can forget about function names, and it's just as if it was all straight line code.

TJ: So the second step is unrolling loops where basically we take a loop in the form of while x… something and we just turn it into a whole bunch of if statements. And realistically, each loop is going to be unrolled to maybe 100, maybe a thousand steps depending on your application. So if you actually took the program and you printed it out, it would suddenly become very long. But luckily, the SMT solvers are fast enough to handle surprisingly large formulas

TJ: And so single static assignment. This is the part where we really take the sort of directionality inherent in executing code and transform it, translate it to the logic layer, which has no inherent directionality. So from the SMT solvers perspective, the logic formula does not happen in any particular order. So we need some way to structure the formula to maintain the order of the program. And the way we do it is by turning every single variable at each time step into a new name. So if we take X and then we set X or something new in the formula, we would have X0 and then we would have X1. And we have a constraint that says, oh, X1 is equal to X0 + A0. I mean, if anyybody here has taken a compilers class. You've probably seen SSA before because this is an intermediate form used by a lot of imperative compilers and it happens to be a really good fit for expressing as the formula.

MB: Every time I watch this talk I get more out of it. So this week I wanted to chat with Tikhon directly about how to model programs in SMT and about the parallels between SMT and the intermediate languages of compilers that use the same principles.

MB: What you talk about when you talk about this— when you gave this talk at Campose, is this idea of translating a program that you've written in a particular language, you used a very simple language in your example, which I appreciate, because I'm also writing a very simple language so I was like goodie!

MB: and then following this process that is very similar to the process that the compiler kind of goes through anyway. This idea in-line creating fresh variables for everything, unrolling, kind of getting rid of loops and creating these nestled if statements instead, and then single static assignment, which I think is the one that kind of pops for people as the most. “Oh, wait, hold on a second. This from here is also from over here” sort of thing. And like I always— like from the perspective of an SMT solver. Well, the thing that was the most valuable for me to understand is that you are doing this, you're flattening it out because essentially it needs to see every part of the timeline all at once. You have, like all the states all at once, like that was the thing that took me a really long time to learn with other formal specification languages is that, like, you're not thinking about it in terms of this kind of linear progression you're thinking about in terms of like almost like string theory of computer science, like all the states exist at once. And we must program in a way that facilitates all the states being programmed at once, I suppose.

MB: Because you started with a very simple language in this talk, where is the ceiling for this approach? Are there like— if we tried to do the same thing in something like, I don't know, for example, Ruby, like, would there be certain constructs that we just can't translate to Z3?

TJ: Well, that's a good question. And I think there's kind of two different questions there. Z3 itself, at least when done this way, knows very little about the actual language that I'm converting from.

MB: Mm hmm.

TJ: There's some amount of built-In operations that are designed for use in languages. You know, you have these logical operations that corresponds to bitwise arithmetic, for example, which is clearly put in there to help people model programs. But for the most part, it's just a way to solve big logical problems. And what that also means is that we actually have a lot of freedom in how we do the encoding. In this specific talk I went to over one way to encode code at a very low level where we're kind of manually setting out a whole lot of these bit vectors, which is what they call, you know, just words made out of bits and the connections between them. And so for something like a Ruby program. You know, even there there's probably these two different approaches to try to model it in Z3, one of which will actually be first compiling that Ruby program to something very low level that talks about how the memory is moved around and what the actual logical operations are, and then modeling that in Z3. And a different one would be trying to figure out how to use the various logical theories that Z3 offers, and just as an aside, the word theory in SMT, which is stands for satisfiability modular theories, Modular theories always confuse me a little bit.

MB: Yeah I was just about to ask what is a theory in this context?

TJ: Exactly. And this specific case, a theory is sort of a set of capabilities that the logic solver can work with. Or maybe a different way to think about it. It's the kind of constraints or the kind of operations that the solver can can consult. And so at the very extreme you could imagine having a SAT solver, which literally only gives you boolean operations. So you have like variables X, Y and Z, and you can just recombine them and clauses using essentially AND, OR, and NOT. And each variable, X, Y and Z can either be true or false, and that just gives you a SAT solver.

TJ: But then you can actually take this the basic logic of just essentially literally one bit per variable and add capabilities in different ways. So the example that I used in the talk was this thing called the theory of vectors, which is basically lets you say like, hey, you know, X is a variable that instead of being a single, true or false, is actually a vector of, let's say, thirty to thirty two true and false bits with some kind of operations that the solver knows about that correspond to things like, you know, binary addition or multiplication or bitwise, bitwise negation or something. And that theory, I think it's pretty intuitive that you could take that theory and actually compile it back down to just normal SAT. Hmm. Because if you have a variable that has thirty two bits.

MB: Yeah.

TJ: You could also express that as 32 variables of one bit each. Right. And when you have addition, you could actually like the same way that you could imagine writing addition out of logic gates.

MB: Yeah.

TJ: You can actually write addition out of ANDs and Ors and NOTs you know in a way that is just a normal SAT solver can see.

MB: Yeah.

TJ: And that's actually a strategy that is really valuable for a lot of these purely bit vector oriented problems that it's called bit blasting. And it just means you take this bit vector logic and you turn it into raw bits in a SAT solver.

MB: Yeah,

TJ: but SMT solvers have a lot of other theories that aren't amenable to this. A really simple example is that some solvers can also support doing reasoning with unbounded integers. So you're going to variables that can be any integer of kind of any size. Yeah. And in order to handle that, there's no clear way, or at least as far as I know, there's no way to express that as a small set of or any set of individual true and false variables combined with these operations. So instead, SMT solvers need some extra logic in the solver to know how integers work, how integer operations work, and how to do like symbolic reasoning or symbolic algebra with integers.

TJ: And then under the hood, and this is kind of an approximation, but my understanding is what happens is that, you know, they have this kind of logic to deal with integers or with other kinds of theories. But then they take the problem that you set up using integer variables and booleans and whatever else, they break it up into cases and then they kind of they can solve individual cases using these specialized solvers that can deal with integers and so on. But then they can solve sort of the relationship between the different cases using the underlying SAT solver or a SAT solver like algorithm.

MB: Through out this series I have had several conversations where one off hand comment created such a powerful moment the whole rest of the interview could be wasted and it would STILL have been 100% worth my time.

MB: I had one of those moments here … do you get it?

MB: It should have been obvious, but I had honestly never thought about it because modern day high level programming languages have so many layers of abstractions but— basically any programming construct can be expressed in Boolean logic because the processors that sit inside our computers and execute these programs are constructed with a series of logic gates. Therefore a tool like SMT, which is essentially just a solver for Boolean logic puzzles with a bit of syntax sugar added to it can model anything if you compile it down at a low enough level. Anything that Z3’s robust set of abstractions and builtins can’t represent, you can just move to a lower level of abstraction, get a little closer to the chip and model that instead.

MB: It’s weird I have been trying to get good at thinking about code for formal verification for years. I never imagined I was going to get better as a modeler by trying to learn how to write a compiler. But life is strange sometimes…

MB: So on the subject of intermediate languages, I’m going to ask you a question that may not be possible to answer, but why does it seem like no matter how fast the computers get, no matter how complicated or sophisticated they get, the end of the day, it's always compiling down to these very simple procedural based steps?

TJ: Yeah, I think that's a good question, and I think it's a lot more an answer about how the market works than anything else because. You know, at a low level, and I am very much not an expert in computer architecture, but essentially the incentives for the people making CPU's right is to be as fast as possible and kind of as energy efficient as possible and to do a good job with this massive amount of existing software in C. And in some cases, I think probably a lot of cases they have to do a good job on software that's already been compiled.

MB: Yeah.

TJ: And so what happens is then the actual the low level CPU's these days with things like out of order execution and these like fancy or not fancy, but like relatively loose memory models and so on, they don't really act like a sequential processor.

MB: Mm hmm.

TJ: What they act like is some kind of dataflow system that is doing its best to appear as sequential as possible while still getting the advantages of a data flow system.

MB: Mm hmm.

TJ: Now, I think even in a different world, we'd still want a simple low level language to work with. But if there wasn't this constraint of trying to work with the existing world of software, it's not clear that the low level languages would look exactly as procedural as they do now.

MB: What could they look like?

TJ: Well, this is where I think it's really worth talking to, that people have a much better understanding of computer architecture. For me, you know, like this research project I mentioned, we worked with a chip designed by, among other people, Chuck Moore, who was also the creator of the Forth programming language.

MB: OK.

TJ: And now that one is still procedural in some sense, but it actually had a stack in hardware made out of registers. And so programming, it felt really different from programming a more traditional register machine.

MB: Yeah.

TJ: Was kind of different, you know, different constraints and some advantages and disadvantages. And I don't know if that's an example of something that, you know, if all constraints were freed, we'd want to use for sort of, you know. High energy, high speed kind of general-purpose chips, but that's at least one example of where. You know, you could imagine a different architecture, but. I've I think probably the best place today to look, to see how things could be different is to see which ways people are taking advantage of FPGAs.

MB: Mm hmm.

TJ: Because, again, like, I actually haven't worked in an FPGA project myself, although I kind of imagine I will at some point. But my impression is there that actually pushes people to essentially view their programs as a lot more sort of data flow oriented, even at the very, very low level of, you know, configuring the hardware that runs on compared to running on a general-purpose chip.

MB: I had always assumed that the challenge of learning to think in formal logic in order to write models that could verify systems was necessary and unavoidable. But in the course of our talk Tikhon made a historical comparison that changed my mind….

TJ: In Z3, when you're working with it, it really does feel like you're trying to figure out how to take your problem and then encode it in this, you know, given this kind of set of logical primitives.

MB: Right.

TJ: It it feels a lot like the compiler whereas Prolog is flexible enough and higher, you know, sufficiently higher level than Z3 that it actually feels like you can write code directly in Prolog, you know, and it feels like using a normal language that has this weird, logical paradigm.

MB: Yeah.

TJ: Once you've got your mind around to it, you know, you can use that as a programming language pretty easily. Whereas even though you could write maybe these SMT lib style formula, you know, formulas by hand and Z3, it still feels like you're mentally taking the things you want to write and figuring out figuring out how to encode it with these primitives. So in some ways, it almost feels like the difference between writing in a a higher level language and writing in assembly where in the higher level language, you know, it's really oriented around helping you express your thoughts on abstractions.

MB: Yeah.

TJ: Whereas in assembly you're the one kind of translating from those abstractions to the set of instructions that you have.

MB: Yeah, that's funny actually. I think that's a really good point, that a lot of the angst we're seeing now in the formal specification world is because of a lack of high level languages that allow people to express themselves without having to do that translation into how the logic, whatever the engine behind it, thinks about things very similar to the era where everybody wrote everything in assembly. And then people who who do high level languages were inferior programmers because they weren't really understanding what was going on.

MB: Current formal verification languages focus their expressiveness on condensing what should be hundreds of lines of logic statements into short human readable phrases… And that’s important! If you’ve ever tried to write a Boolean formal in Conjunctive Normal Form by yourself you understand the value of having a higher level language to do it for you! The simplest problems become an overwhelming amount of code really fast.

MB: By most formal verification languages do not do much to help programmers figure out how match challenges to approaches in formal logic. It would be like writing a high level programming language and not including any abstractions around arithmetic, instead assuming that the programmer should know how arithmetic works in binary and write expressions based of directly manipulating bits.

MB: What strategies are there for making sure that you're producing the most optimal SMT expression when you're using something like Z3, right?

TJ: Yeah

MB: Because there are always a bunch of different ways to write same thing. And some of them have better runtime performance than others, right?

TJ: Absolutely. And unfortunately, actually, this is the one place where I really don't don't have a good answer to. You know because when I did it there was a lot of guess and check, but I also talked to a lot of people who were actively doing research on programs synthesis for example, and it felt like even to people with a lot of experience, you know, maybe they over time developed some kind of internal mental model. But the performance of the solver was still often kind of a bit of a black box to them.

TJ: And my impression was that, you know, the only people who really did better than this were the ones who wrote their own dedicated solvers for solving their problems, or wrote dedicated algorithms to answering specific program synthesis problems. But unfortunately, like figuring out the best way to encode something for Z3. I think it's just something where you just have to spend a bunch of time giving it a try. As far as I know, there's no really general-purpose approach,

MB: Run in some old fashioned performance tests where we just run the SAT solver a thousand times and see what the average it returns and like see if we can beat that time?

TJ: That's right. Although I think usually the difference is less than— it's less about the small differences and more about like, you know, if I run this, will I get an answer or will get bored while waiting for it? Some of these things. I've seen examples where different ways of encoding it take a problem from, you know, like the same problem encoded in different ways. Yeah, sometimes in ways that are actually logically equivalent to you but are different to the SMT solver. And it goes from being like a ten minute solution to being like a twenty four hour solution just because the SMT solver gets the heuristics, get trapped in the wrong part of the search place or something.

MB: Hn. You don't by any chance have an example of that do you?

TJ: So the details are kind of old. But I think one specific example I remember is. I was taking this kind of seminar on program synthesis and one of the homework assignments. You know, it was a pretty, you know. a pretty reasonable problem, which is basically, hey, you know, we talked about how you would encode a certain problem as a simple formula. So here's something really similar. Can you go at home and encode it?

MB: Hmm.

TJ: And, you know, people came up with reasonable solutions, but most of them like, you know, I mean, also, just to be clear to most people, also waited until the last day to do it. The problem was that, you know, people came up with good solutions that actually didn't even finish one run overnight before the deadline.

MB: Oh, my goodness.

TJ: And in that case, I think it actually took the professor and some of his, you know, a senior graduate student some time to figure out what was going on. And I think it just turned out that, like, you know, we used it like people used a reasonable subset of the SMT operations, but they needed to explicitly tell Z3 which theories they were using and which ones they weren't in order to get it to work faster.

TJ: And I think another maybe slightly like that one, that's kind of forgivable in the sense that, you know, you can kind of see the Z3 default mode trying to be more general-purpose and therefore slower.

TJ: But I think another example that would throw me off, but I've heard people mention is that there's actually a difference between making a single assertion with a whole bunch of ANDs in it versus making a bunch of assertions in a row, even though, again, semantically they should be the same.

MB: Yeah.

TJ: And again, I don't know if newer versions of Z3 handle this better, but, you know, there were some people who you know, I saw some very concrete advice that said, hey, you know, if you're using the theory of a raise and you need an array where you need to sort of initialize it with a bunch of values, then it's better to have a bunch of individual asserts like assert that index one has value X and index two has value Y instead of having a single big assert with an AND in it.

MB: Yeah, that's an example of where it's very much. Some kind of detail of how the salver processes formulas and does the search that leaks out into the performance characteristics, because logically those two should be exactly the same.

MB: My first couple tests of this concept of compiling to something like Z3 didn’t involve an intermediate language between my type checked AST and generated SMT code. I wanted to see if I could generate things that ran on Z3 and get my bearings.

MB: But given the how variable performance can be given different equivalent constructions, it’s clear I can’t skip the optimization stage of compiling. So I need to develop an intermediate representation from my AST that my compiler can analyze and modify.

MB: The other thing I need … some way to handle floats!

MB: If you try to represent a number with a decimal point in Z3 Real number types what the solver will return is an expression that divides two integers which would equal the value of that decimal….. a literal fraction in other words.

MB: This makes a lot of sense but also I’m not sure how it will scale. There are other approaches to decimals. Another friend who’s savvy with Z3 thoughts using bit vectors would kill performance. There’s support in Z3 for floating point arithmetic now… but honestly I’m not sure I understand how it all works from the documentation.

MB: Somehow I feel like the easiest thing might be to make Fault fixed point, where every number is represented with two integers: the value written out as if you just erased the decimal point. And a scope in base ten specifying where the decimal point actually is positioned in that number.

MB: Will this result in faster models than something more direct and built into Z3…. not sure!

MB: You mentioned in your talk that four are floating point numbers are difficult in verifying programs, that the programs are verified using real numbers. Why is that?

TJ: Yeah, well, it's also I think this is kind of the same thing I was saying. And I guess I'm not sure what kind of what the state of the art is necessarily in a lot of areas. But it's just if you want to figure out some mathematical properties of some logic, it's much easier to prove those properties on top of real numbers, which are, you know, well behaved mathematically than it is to kind of do the numeric analysis to understand exactly what happens with floating point numbers.

MB: Yeah,

TJ: And to be clear, there is a whole active area of research and practice around numerical analysis, and there are some really good tools to help with that.

MB: Yeah

TJ: But it makes, you know, using other kinds of verification somewhat harder if you have to deal with exactly the kind of, you know, bitwise operations you get with floating point.

MB: Is it because you can always add another place behind the decimal?

TJ: Conceptually that's exactly why real numbers are so much easier, right? And that's because you don't have to worry about all of this potentially complicated sort of rowdy behavior. And also just in general about the exactly which values floating point numbers represent. Yeah. But also because with real numbers, you can basically bring to bear continuous mathematics onto your problem. And that's a field that's been studied very extensively and so there are a lot of good results and are really nice properties that continuous functions have, for example, that other functions don't.

MB: Yeah

TJ: Whereas if you really, really care about exactly what a floating point number of program is going to do. You know, thinking about it as as implementing continuous functions doesn't really give you the full behavior, especially kind of as you go further from the the the the kind of numbers that floating point numbers represent well.

Uncertain Types part 2 (featuring Barak Michener and Eric Schles)

Marianne — Wed, 31 Mar 2021 03:57:19 +0000

Summary

Still struggling to understand how to implement uncertain types, Marianne calls on two friends to sit down with her and brainstorm different approaches. It looks more and more like adding uncertain will cause the language to scale to unpractical levels of computational complexity… then suddenly Marianne has a stroke of inspiration that changes everything.

Links

Uncertain: A First-Order Type for Uncertain Data
Barak’s Draft Implementation
Official C# reference implementation
PGMpy

Bonus Content

Become a patron to support this project.

Transcript

MB: Welcome to Part 2 of my episode on Uncertain types. The goal of implementing uncertain types is to build models that estimate system fragility … in other words, not just whether a constraint can be violated as with formal verification, but an estimate of how likely that violation actually is. My thinking is, fragile systems will have lots of paths that end up violating a constraints, small changes in one part of the system will compound easily into undesirable states.

MB: Resilient systems, on the other hand, will have few scenarios that violate constraints and those inputs will be unlikely.

MB: If I’ve lost you already, I would recommend going back to some old episodes. Specifically episode 02, episode 07, and part 1 of uncertain types last week’s episode.

MB: In that episode I did a deep dive on probabilistic programming, we heightened my anxiety around creating these kind of models with the approach laid out in the Uncertain paper from Microsoft Research. Using probability distributions feels like the scalpel— no, change that. It feels like a robot laser. Not a tool for every problem. The approach may only work for a subset of use cases that are not relevant.

MB: And even if I understand the math well enough to use the techniques effectively, my language will have to help the user understand the appropriate way to build models. A tool that helps people come to false conclusions is not a helpful tool at all.

MB: So I needed to call in reinforcements. Luckily I have friends who were willing to give their time to brain storm solutions with me.

MB: Do you two actually know each other? I know kind of like both in the near tech scene for a while, OK. cool

BM: Yeah. For a minute there I was. I'm living in New York from 2013 to 2016.

ES: So, OK, I believe the time frame I was a social person then. I don't know. I'm Eric.

BM: Yeah. And I'm Barak. So.

ES: Barak … OH really?

MB: I swear to God I did not realize their names rhymed until that moment. Now there are three things we are going through as we talk here, all of which are linked in the show notes on the Dev Community.

MB: First is the Uncertain Types paper. Then there’s an example implementation that Barak started working on when I told him what I was trying to do. Lastly there’s an example implementation in C# from the authors of the paper. This may be a little tricky to follow along to, but I’ll do my best to fill you in on the missing details.

BM: It's all coming back to me… ummm was that…. There's no magic here, though, I just. OK, it’s— ah, sorry, I'm going to make noises as I remember what I was up to. So from the reference implementation, the way the reference implementation works is that they have their basic unit of something is the type in question and a weight. I think and so everything feeds forward and the way they're doing it is they're using a LINX in C# to. Essentially read the queries and the for loops and stuff that I'm going to do manually anyway and.

BM: Generally speaking, the idea is that if you have to and this is often the best part of the paper, there's one part of the paper….. I remember being really, really helpful here. Let me see if I can do my thing here at. Uh. Yeah, OK, here's where I left off last night on the other stream…

BM: I can still hear you won't be able to see it because KVM which on and I think I still have that window with all the stuff in it open.

ES: Ahh, it's a little fuzzy.

BM: Sure, let's see if I can see where I left myself off, if I let myself off anywhere.

MB: Oh, my God, I thought I had a tab problem. This is insane.

BM: Yeah, I think I've already cleaned up since January it’s been bit… Anyway. Let's see there…. Pull up the paper.

ES: It's in the invite.

BM: Here's the reference. Implementation is at least in my history. Yeah. And, uh, let's see, um.

ES: It's in the calendar if you don't remember it,

BM: Ah! there it is, Microsoft Research. The most useful bit of this entire paper for me was this little thing right here.

MB: What he’s referring to here is a figure called UncertainType operators and methods. Which groups operators into Arithmetic operators (plus/minus), equality operators (less than, equal), logical operators (and, or, not), sampling methods and hypothesis testing. Then the figure specifies what types come in as input and what types come out as values.

MB: In other words: if you write uncertain typed variable A is equal to uncertain variable B what’s return is not a True or False, but a distribution of Trues and Falses …. right?

BM: Idea being that there are. Two or three different types we're actually talking about here.

ES: Yeah,

BM: One is this is the general and uncertain type of type T. In general type T ends up being mostly a float, right?

ES: Yeah. Basically,

BM: Bernoulli is a uncertain type only where this is a bool.

ES: Right.

BM: And again, this is sort of a float, if you representable is like a 50 50 thing or a weighted thing. But let's go with the bool for the moment and then a sampling distribution is the same thing, except for there are no. It's literally just a materialized array of. Values,

ES: Right

BM: Where these are populations, this is this population statistics like median mean and standard deviation right here. This is actually just a real list of values, whatever they may be.

ES: Yeah, right.

BM: Cool. And this all works very well as you move as you kind of move things forward or if you run through all these operators and even the sampling methods outlined here. Because you can sample things and you can combine different things, and it's an optimization to say that I can combine the means and standard deviations if there's a meaningful way to do so.

ES: Right.

BM: If there's an equal quality, obviously says yes, either boolean output. So that's why this is an output. Same with logical things. If there's no good way of doing so, we just sample the heck out of it. And you could then turn that back into a thing. Sort of. Kind of. But then you're losing something. And I didn't go that far.

MB: So that that was actually one of my core questions with like implementing this for my purposes. Right? Is that my feeling for reading the papers that the bulk of the what they were talking about was assuming that you're dealing with independent variables. And because I'm constructing a model, they're all dependent variables right? So they’re sort of talking about like this is how you do it, dependent variables. And they've lost me a little bit on the math there. But I was actually wondering, like, is the best way forward to figure out how to represent these probability distributions and do basic operations on them? Or is the best way forward to actually have the distribution and then when the model is running, draw like a certain sample of likely values at a certain example of unlikely values and then run the model a bunch of times with those values to get to the the same conclusion that I want, which is like how much of an impact is an outlier value have in the performance of the model?

BM: ……Let's take that sentence, that's a very good sentence, I think that will cover like the entire hour and more. So let's try and take that down piece by piece.

BM: So independent and dependent variables. And that's the conditional probabilities. I also had trouble with because I wanted to say was what I was trying to figure out that I kind of only got part of the way into before I needed to really refactor. Everything was the whole trace of how I got here. That's how I was implementing it. That may not be the right way to do it, but that's the way I was thinking about it.

MB: OK.

BM: Which is I could instead of imagine, these are like all things that are flowing through each other, right? Like I have an AND operation and then an OR or whatever. And there's all they’re independent in the sense that I don't have any memory on them. But if I add memory to them, so I say, OK, I initially sampled this from here and it had this value here. And because it had this value here, it had this value here and then it had this value here after I did this to it. Right? Mm hmm. And then I have an output sample where the sample give me its entire history of how it got there and all the variables that it went through to get there. Yeah. Then I can write a function on saying, OK, well, look at your history and tell me based on your dependent, like based on the thing that I'm depending on. Whether I wanna do this or not. So this is. And this is where they were using LINX to effect in the C# implementation is essentially this is a where clause on the history. It's a thing where …..let’s see, because I know all the history and everything, and I'm doing something like. And probability of X given Y and Y is somewhere in the chain of X, I can then say, OK, I'm going through all the X is find the cases where that Y was true because it's in the history of X and then that's my sample. I reject anything else.

ES: Have you ever seen a probabilistic graphical model implemented?

MB: I’m just going to say no, because I know I have never seen that

BM: I haven't.

ES: Ok, so PGMs literally, that's the goal of PGMs, right? You start with—I’ve implemented PGMs before. They're really,,, you know, they're kind of trivial. So in the paper, they talk about Bayesian networks. Right? Like, Uhhh… I got to pull it up because. I know. I mean, so like somehow this paper was very confusing to me, honestly, because they like mentioned Bayesian networks a bunch of times and they’re just kind of like ….. “look at all these machine learning things, look at all these machine learning things.” They never really I don't know. It was just very confusing to me. It's like you're not giving formal definitions of anything and you just keep mentioning the benefits. And it's like if you repeat it enough times— see we introduce a Bayesian network, semantics and like, they use this a lot, but they never really define a Bayesian network beyond, like, some trivialized thing. Right. So, like, this is what they're saying is a Bayesian network, but ….not really.

BM: Right.

ES: Yes. You know, this is this is like their notion of addition. Right. And so if a… if these are not independent, like if you have one Gaussian and it's conditional on another one, then like you would just you can just implement a PGM. So, like, there's you know, I worked on PGMpy back in the day. So like this, I mean they change the reference API so much since I contributed to it. But I think it's still I think it's still in here. The thing I wrote but I would look at this like this is this is like a good place to go. If you want to understand how the conditional probabilities are going to, you know, connect. Yeah, the PGMpy’s implementation is is is perfectly adequate, I think, for your for your needs, for conditional probabilities. And then it looks like, Barak, it looks like you've got everything else. Just chain through that. Then you're set. I'm going to try to reason you through it, but I'm going to fail. Probably just …..crap, I haven't looked this reference implementation in a long time. It might be too hard for me to walk you through what they have. Yeah, OK. They've really clean this up. When I did it, it was garbage.

MB: WellI, I will point out that the wonderful thing about GitHub is that you can go to history and find the garbage that you checked in that you might be more comfortable walking us through.

ES: Ohhhh no one wants to look at my garbage code, you don’t want to look at that.

MB: Just a thought!

ES: I know but we don’t want to look at that.

ES: But so, like, I have a question and this is important. Are you trying to do a truly Bayesian, you know, regression model or do you want to trivially just sort of like take a maximum likelihood estimation?

MB: I don't know, because I am not entirely sure what I'm doing. So, OK, this this is kind of like basic, completely pointless model that I sketch out. Right? And this is what I'm trying to represent in code this idea that you have certain stocks that have certain units of value in them and then you have the flows that are basically rate of change going from one stock to the other. All this is great, super easy, love doing it. But the reality of it is that a lot of times the stuff I'm trying to model, like, I don't know, an exact value, that's not a realistic component of the model, but I know what a likely value is. Right? I know what an unlikely value is. So I thought it would be interesting to sort of inject a little bit of probabilistic programming into it and allow people to express models by taking values and saying, like, look, I don't actually know what this should be, doesn't have a default value, but I have a probability distribution of what the potential values of this are. And give me some— I think essentially the big thing that I'm curious about is can…. A model run with probabilities kind of give you an idea of how stable the model is, right? So that question of like how far away from the mean. …can you get before you start, the rest of the model starts to get into an unsafe state, and how likely is that?

BM: Another version of that question is how far away does it get from the initial conditions? I'm sorry.

ES: Yeah, that's for sure. But, um, I mean, it sounds like you want to Bayesian like you just want you just want you just. Yeah. You just want a Bayesian model. So the right thing to do in that case is you define your distributions, right. You have your distribution types and then you just have a sampler that samples from your prior distribution, which is what you would encode and gives you a posterior, and then that is your area boundary around your model output.

MB: Yeah, so that was sort of the question I was asking in the beginning, because, like this this model will run for, let's say, five steps, which means all of these rates will execute five times to all of these units will change depending on the rates. Right? And so I was looking at this in terms of like, well, we can keep if we say that this this big stock right here is like a distribution. Right. We could keep that as a distribution and like, I guess alter the distribution, which each iteration of the model or we could say shoot off some potential values, given the shape of that distribution and run that model with those potential values and say, OK, this is what this model looks like with the like highly likely values, and this is what it looks like with the outlier values. And this is the difference between them. I'm not sure which one is the more sensible way of going. I know which one is—

ES: They’re both sensible. It just depends what you need. Right. So, like, OK, so, you know, frequent statistics, right? We just we just literally take the maximum likelihood of our distribution. That's what we do anything. And that gets us most of the way. And then you put confidence intervals against some things sometimes. And that's like how you measure uncertainty in your model. Right. And that's it. Like and then the Bayesian approach is you start with the distribution, you sample against it, and then you get a posterior and your posterior. If it's the right, you know, prior distribution, like going into your thing, you as a as a matter of course, for your optimization strategy, you end up with a like a posterior that like is small and gives you reasonable our error bounce. And then it's just obvious what your like prediction is. So both of those things are reasonable. It's a question of what you want and it's a question of like what makes sense for your setup.

MB: I think….. So what I what I want to answer that in the easy non-math way is the ability to find situations where you have one part of the way your models configured that is really, really volatile. Right. Like you're hanging by a thread here that value wobbles just a little bit, like the entire model's behavior shifts pretty dramatically.

ES: Are we talking a statistical model? I just want to make sure on the same page.

MB: Not a statistical model, they're called compartmentalized models, which is not useful. It's like it's just a system model.

ES: Ok, all right, I'm going to say I'm with you now. Thank you. So you've got some… OK, so you're talking about modeling physical systems with probabilities.

MB: Exactly.

ES: I mean, I think you should just model it as a PGM.

MB: OK

ES: Really what you want. I think you are literally just doing a prediction on that. Given all this conditional probabilities will literally return to you, the state your overall system risk, because it'll like it'll predict it like, you know. So, yeah, because you just said, like failure, like your failure condition to be like true. And you're like success conditioned to be false or vice versa, depending on how you feel that day. And then you just literally do a prediction. I mean, you could use a neural network, you could use something else, but then you don't have it's not obvious how your system is going to operate, you know. So, like, I see why you looked at this paper because you wanted an uncertain type. But like my my honest recommendation, you need to go a step further. You really should just be thinking about this in a model context.

MB: Yeah. I mean, I think I generally follow what you're saying. I'm just trying to, like, process this from a parsing standpoint. All of this information will be in the model, but it will be determined by the person writing the model and then like getting the compiler to then essentially encode that into how the model runs. I, I feel like I have to like have a montage of me in a library somewhere, like digging.

ES: I shouldn't be. This shouldn't be this shouldn't be that hard. Right. You just have an implicit you just have an implicit statistical model embedded in your compiler that like does the prediction. So really you just need a reference implementation. There's not it's not more sophisticated than that if you pull any reference limitation. And I'm not claiming that, like the PGM model is definitely the right one. I'm claiming I think it is. I you know, obviously you need to consider this further, but some statistical model should just be embedded in your compiler. And like, literally, you're just running a model and that's it. Like you're running a statistical model over this space and the engineer encodes the probability distributions. And then either you return a Bayesian thing or you return to frequentency things, either returning, you know, this is the probability of success and this is the probability of failure or they're returning a distribution. It's like you're the the cases where you fail here, the cases where you succeeded.

ES: It's that simple.

BM: There's maybe actually in this case a little bit with the the paper itself is what you and this is just thinking. If I were writing in your language and trying to build the building model with these things, what I would want is a is a failure predicate. I want to be able to say—

MB: Right.

BM: This is what a failure looks like. It's when, say, this box here on the bottom right is totally empty or something like that.

MB: Right. Right.

BM: And what we're doing then is this of simple case is like, OK, everyone has their initial conditions and we just run it forward with integers and everything is fine and we can tell if it hits that point. But then you're asking is OK, if I have a distribution of these things and if I do, I ever hit that?

MB: Yeah,

BM: and that's similar to a PGM I think where I'm tying it together now is then. You can sample the heck out of it and some of those will fail and some of them will fail with some amount of probability and you can tell the user then what failed? And then also this goes a little bit to my history thing, but not entirely. But it's kind of it's all about conditional probabilities where you can say, OK, for the failures. What I saw was here were the other states I started with.

MB: Yeah, yeah. OK, so it's sort of like in the same way that first order logic and a SMT solver like is does not actually run the model. It just defines a huge number of boolean rules and then like deduces all of the possible states and tells you if you have something that violates your constraint, like the the probability-- the statistical model behind the scenes isn't actually running any of the model. It is simply like calculating the statistical probabilities and identifying places where the constraints are violated. And other conditions are present

ES: A way you can think about it as it's running simulations. Yeah, that's the trivial case. It's just it's like literally it's actually trying things like from a sampler and it's just literally saying, OK, so here are my parameters on my distribution. And then like, I'm going to just run a bunch of cases and then we're going to see what kind of probabilities I get to see what results I get back. That's Bayesian samplers work. That's how Bayesian statistics work. So, you know, that's all you're really doing. So you just like try to model a bunch of times

BM: Yeah so you run your code forward. You've already got it working for the static case of a single integer. So just run it with a bunch of different integers.

MB: Ok, yeah. So that is what I started thinking around the second option of just pulling a sample and running the simulation a bunch of times. That's essentially what we're talking about. I just didn't know any of the fancy words for it. Damn it.

ES: I mean, academics need to get paid somehow, right? So I'm teasing all these terminologies are actually super important, but like, yeah, I can get really confusing. There's just a lot to think about.

MB: So now my question about this approach is, since it's based on sampling, does this get more and more complex if we add more and more uncertainty to the model?

ES: Well, I don't think so. I mean. I don't think so. I don't think so.

BM: I mean, as the model gets bigger, you'll need more samples.

ES: Yeah, yeah. I mean, it's expensive computationally, right? Yeah.

BM: I mean. For a lot of these things they had, that computational cost is a part of the business of doing models and B…

MB: Yeah, I kind of want to stop short of the this language can only be run on GPUs that you pay like millions of dollars for.

BM: I don't think you're going to run into that soon.

MB: It's true. This is true.

MB: But you know I wasn’t satisfied with this answer. I’m okay with a little resource intensive, most formal verification is a little resource intensive, but I want Fault models to be runnable on normal machines. I want models too big for a single laptop to be really truly outliers.

MB: So I kept thinking about how to break the model up into smaller runnable parts…. like could we structure models into modules that in effect act as black boxes to one another? Each flow is a function where … maybe… we calculate the range of possible return values given whatever uncertain values are in scope—HOLY SHIT.

MB: Holy shit! Guys wait… Holy shit I think I’ve got it. I can take the flow’s function and represent it as SMT. A logic puzzle like normal formal verification. But if there’s an uncertain value, the compiler will generate SMT that solves for that value, negating the assertions so that we’re looking only for scenarios that result in an undesirable state.

MB: Then we can take the probability distribution and the solution presented by the SMT solver and see what the odds of our uncertain type actually having that value.

MB: I think that will work … more to the point: I know exactly how to implement that!

Uncertain Types part 1 (featuring Maria Gorinova)

Marianne — Wed, 24 Mar 2021 03:00:05 +0000

Summary

Equipped with new knowledge about type systems, Marianne begins speccing out plans to implement uncertain types and inject probabilistic programming into Fault models. She picks the brain of Maria Gorinova—researcher and probabilistic programming evangelist—and wonders if she’s finally bitten off more than she can chew.

Links

Maria Gorinova’s Website
Stan programming language
Uncertain: A First-Order Type for Uncertain Data

Bonus Content

Become a patron to support this project.

Transcript

MB: Okay now we know how to do types … maybe.

MB: Here’s what I want to do with types in Fault. First I want to implement a natural number type. There are plenty of system models where it’s illogical for a value to go negative. You can’t have negative people, for example, so it makes sense to have a type to express that.

MB: The big challenge I want to conquer, though, is uncertain types. This concept was first introduced to me through a paper from Microsoft Research called Uncertain: A First-Order Type for Uncertain Data.

MB: In this paper the researchers describe the implementation of a specific type that represents a value as a probability distribution. You initialize it with a mean and a standard deviation, and then can perform certain operations on this data type.

MB: The reason this idea was attractive to me goes back to the fundamental problem with modeling the behavior of feedback loop systems using formal specification. Formal specification answers the question whether a state is impossible or not, but there are lots of states that are possible but dangerous in a particular context. In those cases we want to know how likely a state is and how much change the system can toleration before an undesirable state occurs.

MB: Uncertainty would be useful here, but as I read (and reread) the paper I realized that I felt a little shaky on my fundamentals. This is the world of probabilistic programming, and rather than making a dumb math mistake by jumping right in maybe it’s better to get an overview of probabilistic programming itself.

MB: So I called in an expert…

MG: My name is Maria Gorinova, I'm a student at the University of Edinburgh towards the end of my Ph.D. So fingers crossed. I work on probabilistic programming and more specifically, I mostly working with Stan.

MB: Okay so what do I want to know? Ugh… there’s so much!

I’m I reaching for the right tool? What is probabilistic programming used for? Maybe my use case for uncertain data types just doesn’t make sense … I mean… does the whole model have to be done in probability or can I just drop one uncertain value and everything stays kosher?
Is it really true you can add and subtract (maybe even multiple or divide) distributions? What are the conditions behind that? Only normal distributions? Only with independent variables like described in the paper? This idea of doing operations on probabilities seems like black magic
Where are the pitfalls? I know this can’t be as straight forward as it seems. What am I missing? What are the gotchas?
And lastly … if this can be done why hasn’t anyone done it before?

MB: If I can figure out what can and cannot be done with a probability distribution, then I can start thinking about how to represent that in types. The operations is the easy part. I can write those restrictions into my type checker and invalidate models that perform unsupported operations on uncertain data types.

MB: The authors of the paper do have a reference implementation in C#. It took me a while to track it down, but it’s up on GitHub. Unfortunately so much of the logic is imported from other libraries it doesn’t clear much up. It seems like this problem might take more than one conversation to tackle. So I best use the time Maria’s giving me to the best of my advantage.

MB: Ok, so, I mean, I guess the best place to start is just with the absolute beginning, like what exactly is probabilistic programming?

MG: Yeah, that's a very good question. And I like to think about probabilistic programming as in a sense in inverse programming. So in conventional programming, you would write a function where the function takes some input and the entire job of your coding and of your program is to produce an output based on this input. Right? But in probabilistic programming, you really that is that you in a sense write a model which describes how some data was generated.

MG: So you still start from some inputs. But this input is unknown and you put some probability distribution in it and then you sample random variables inside of the program and at the end you spit out data. And what happens is that you actually have this data, you've observed this data, and now you want to model the parameters it was generated from. And by model, I mean, you want to compute somehow the idea. You want to have uncertainty over your belief about these parameters. So you want to compute the posterior distribution where you can say, oh, I know the probability that this parameter mu that's the mean of my data will be smaller than zero is 90 percent or something.

MB: This sounds perfect right? Quantifying uncertainty? Check! Running a program backward so that you get the inputs that will produce a particular output? Check! It feels like there are a lot of places where programming with probability would be useful.

MB: As it happens, Go has a package for probability distributions under the stats section of gonum … it has a couple actually, depending on whether you want to do univariate or multivariate or matrices.

MB: A lot of what people seem to be using it for are random numbers or other to build other stats tooling rather than probabilistic programming. I’m not seeing very many models…

MB: And what are the practical applications of something like probabilistic programming?

MG: Um so it has been it has been a growing area, it's now used— Stan in particular— has lots and lots of users. It's being used in a lot of sciences like biology and particularly evolutionary biology, astrophysics, particle physics. So things like that.

MG: Also, I think it's used in economics and business in general. And so anywhere you have data that you want to learn from, but you also want to have to quantify uncertainty. So in contrast with deep learning here, we are very precise about our research into everything. So it seems everything is statistics driven and we we believe our confidence intervals. So we will say confidence interval interest when it comes to Bayesian stuff. But still. Yeah, yeah.

MG: Well, with deep learning, we can learn from data, but it's very different because we actually trust most of them, we can't really trust what the results… that we can’t trust— no, not only can trust the results, but we can't trust our confidence in the results. When you say, oh, I believe with 90 percent progress that these images are of a cat.

MB: Yeah.

MG: Can be arbitrarily wrong. Like it can be … You know, a bird or something, and it will still be very certain that this is a cat.

MB: Yeah the math part is what I’m worried about. I took some graduate level statistics classes when I got my masters degree. I loved it. I feel comfortable with the concepts … but maybe I know it well enough to know that once you add some programming it becomes possible to create something that seems to produce the correct response but stands on a foundation that is not stable.

MB: That’s the reason why we tell people not to write their own cryptography libraries. Lots of things can look random but aren’t. Correlations can be misleading. It’s so easy to misunderstand a concept and build something that has no real value.

MB: Do people tend to use probabilistic programming sort of just in isolated research cases, or do they tend to do it in tandem with more traditional programming?

MB: So like, for example, something that I do a fair amount of is like logic programming. And you can sort of use logical components within a traditional application to do various functionality, like, for example, policy adjudication. Like you can write your policy server based on an SMT salver using sort of logical programming, declarative structure. And then the rest of your application is just kind of object oriented and it just kind of those two components, talk to one another and work with one another. Is there a same relationship and probabilistic programming? Is it really more like it kind of sits off to the side in a research capacity?

MG: Hmm. That's a that's a very good question. I think currently it's more of a separate thing that is used when you when you have some data and you want to do analysis data. You sit down and write up, probably growing, but. I think the dream is that it's more integrated and it's more accessible as well, because the dream of probabilistic programming is to completely separate the modeling. So this is like writing your belief about how your data is generated from inference, which is the complicated inverse maths stuff.

MG: And this in practice is not really the case. You have to think a lot about what you're modeling, how you're modeling it, is your model correct? Do you make any stupid assumptions in it and so on. And it evolves. It involves like diagnostics and things like that. Currently it's not it's not that accessible. And we're working towards making it more accessible to people who have programming experience, but not necessarily statistics, experience, experience. But it it's it's hard.

MG: It's supposed to be something democratizing that just gives this tool to people that are domain experts in other fields, not statistics, and they can then use it for their problem by kind of inputting their domain knowledge into the program without having to think about anything else. But in reality, there is still a steep learning curve there.

MB: This is starting to feel really intimidating…. I asked Maria about uncertain types and she had never heard of the research effort, which threw a slight monkey wrench into my plans to ask someone to hold my hand through the math bits.

MB: Maybe I’m on the wrong path here? If no one else is incorporating uncertainty into normal programming, maybe there’s a good reason?

MB: Is it that really the probabilistic programming mostly manifests in its own separate languages, or have people incorporated libraries into other languages?

MG: They’re libraries, Yes. although I still call them languages because. Yeah, because they're kind of like almost like a standalone thing. It's it's a little bit like Tensorflow, PyTorch for…. It's sort of entirely new. Yeah. So we have Edward II and Pyro and PMC3 which are kind of integrated into Python. We have Gem and Turing and I think. What else? And….. A couple of other languages in Julia, so, yeah. There are lots of of those.

MB: Hmmm… Julia and python, two languages well know for data science. That’s not a great sign. (sigh) …. but I just can’t shake the notion of leveraging probability. I might need reinforcements. And by that I mean, I might need to call on some experts a bit closer to home. Experts I haven’t cold emailed out of the blue, but people within my friend group who I can more easily lure into hour long brainstorming sessions and guilt into code reviews.

MB: What are the most common mistakes people make with probabilistic programming?

MG: It's very, very easy to define a model that is ill conditioned. So that means that the posterior distribution that is given by by this model and the data you observe… has a very weird form, basically. So. So imagine imagine we are talking about the bivariate distributions. So we're going to do a 2D plot where the color kind of represents how how much probability there is for each of the axis. And now imagine a Gaussian distribution, which looks like an ellipse in this. And if if it's well conditioned, this Gaussian distribution is going to look like a circle like this, because this is it has to do with like the ratio between the smallest and the bigger variance of this axis. So, like the in the larger it is, the more ill conditioned it is. So like, if we have something that is like a circle you have this axis is equal.

MB: Right. Right.

MG: The the smallest in the larger axis. So…

MB: But the like more oblong it is the more ill conditioned it is.

MG: Exactly like this, especially if it's making a diagonal like that and it's very, very, very thin. Then, then the ratio is very big and that's bad. And this has to do with, you know, the statistics, algorithms that we use in order to find a distribution or will have for most anyway will have a problem with this ill conditioned distribution. So you can very easily define a model just right. A model that is going to imply a posture like that.

MB: So not to leave this at a cliffhanger or anything, but next episode is going to be a little bit different. I’m pulling in some friends and we’re really digging into this paper on uncertain types. You’ll be very surprised where it all ends up and hopefully not so overwhelmed by the final math!

MB: To be continued!

Type Systems (featuring Ron Garcia)

Marianne — Wed, 17 Mar 2021 03:45:37 +0000

Summary

Marianne completely underestimates the complexity of type systems and struggled to figure out how inference, checking and conversion work together. After a month of scraping together a smattering of facts, she calls on expert Ron Garcia to help her figure it out.

Links

Ron Garcia’s course Programming Language Principles
Papers We Love: What type of thing is a type?
ICFP 2018 Keynote Address: Gradual Typing

Bonus Content

Become a patron to support this project.

Transcript

MB: This episode is going to be a bit of a detective story. When I first started planning out this block of episodes— should I call this a season? I guess it is! Okay, this season. I looked at the topics I wanted to explore and thought “Oh… well actually some of this stuff is more interesting if I talk about it in terms of types. So let’s plan for an episode about type theory and type checking”

MB: And— as always— I naively assumed that I could just type “how to implement a type system” into Google and piece together an understanding from a bunch of tutorials. Except … no such tutorials exist.

MB: Or rather tutorials do exist but there was a huge gap. I found some great tutorials about typing in general: static -vs- dynamic, why certain languages are stricter than others … these are tutorials designed to teach programmers how to interact with the type systems already implemented by the languages they use.

MB: Then I could find a great set of tutorials about type theory. All the different types of algorithms for inference and math behind them.

MB: But I couldn’t find anything on what implementation of this theory within a compiler looked like. And now I know what you’re thinking: Marianne if you know how to program and you understand the theory why would you need someone to tell you how to implement something?

MB: And the answer to that is type theory is a formal system of logic, so the computer science papers explain the algorithms in terms of logic programming and theorem proofs using languages like OCAML and Haskell both of which have abstractions that do not exist in most general programming languages.

MB: If you remember the episode on BNF grammar, you’ll recall I got myself into a similar situation then. Only this time I didn’t find a secret resource that clearly explained the correct approach and made everything click together. This time I had to scrape together bits and pieces of information, look for the next Google friendly keyword I could use to track down more information. It was a SLOG. For close to a month of reading and searching and reading… it felt impossible.

MB: This episode is that story…

Stage 1: I don’t understand what the phrase Type System means

MB: At various points during my research I would ask people in communities I frequent if they had any recommended resources to better understand type systems. Most of them replied: what kind of type systems?

MB: And truth be told I STILL don’t know what the correct response to this question is. Are you asking static -vs- dynamic? Are you asking what inference algorithm I want? Whether I want Polymorphic types or dependent types or linear types? There seem to be so many options on the type menu that I don’t have a clear sense of what the top level filter should be.

MB: But through searching and not finding what I was looking for I realized that type system is not the correct word for what I meant…. at least not exactly.

MB: When I would search for information on type systems I would get lost in descriptions of type inference, which is a small part of a type system but no where near the complete story. This is like searching for a cake recipe and finding nothing but various opinion pieces on sugar substitutes… then trying to get a clear picture in your mind of the process of baking a cake from reading a twenty page analysis of the correct ratio of agave syrup vs coconut sugar. The explanations I found around type systems tended to skip all the boring foundational components of type systems and go straight for the bits where the most debate and research is happening. Great if you already have a CS degree, frustrating if you’re coming in completely cold.

MB: Basically, type inference is when your program does not declare what a variable’s type actual is but you’re going to infer (guess it) by comparing its characteristics to characteristics of known types which the programming language has defined and which have certain rules. If a variable passes all the rules, it can be thought of as that type.

MB: Type inference is important because declaring types all the time, every single time, can be pretty cumbersome. Remember that’s not just variables, that’s also values returned by functions. Some languages— like Go— have very simple Uni-directional type inference. Meaning that if I store the output of a function in a variable Go does not need me to declare that variable’s type because Go requires me to specify the type the function will return. If a function returns type int, then Go’s compiler can infer that a variable storing the value returned from that function is also a type int.

MB: Other programming languages are less strict about when and how you must declare types … or whether or not a variable can do something like store data of type int and be reassigned data of type string. If you’ve programmed in multiple languages before you’ve likely seen many variations on syntax around typing. The more flexibility you give the programmer, the more complicated and necessary inference becomes.

MB: So when you ask people about type systems they immediately jump to talking about type inference because it feels like the meat of the issue. I see myself doing this a lot with topics that I know a lot about too: I skip the parts I already understand because I don’t remember what it was like to not understand them, I forget they might even need to be explained.

MB: One of the people I talked to in my quest to understand types is Ron Garcia. Ron is an Associate Professor of Computer Science at the University of British Columbia. He’s got a patient and very accessible style but still when I asked him about type systems…

MB: When you explain type systems to people like what actually is a type system.

RG: Right, right, right. So. Basically, so I gave a talk at Papers We Love a few years ago, it was really about it was about type systems, but it was mostly couched in a particular paper, one of the first kind of really serious formal attacks on type systems. It was done by Robin Milner. And like that paper, like really I've read it way too many times, went over my head even more times than I've read it, probably. But but at some point, like, there's a bits in it that you sort of click.

MB: The paper he’s referring to is Robin Milner’s A theory of Type Polymorphism in Programming … so right, straight into the deep end here, but seriously it’s a great talk and you can find a link to it in the show notes at dev.to/bellmar

MB: But as we talked about it more, Ron actually has a great metaphor for thinking about type systems that would ultimately help me break down and organize my research.

RG: It's a number of sentences that you can write about a program so I can say if I have this chunk of code, like let's say I have X plus Y, like, oh, here's a chunk of code. And you're like, yes, that's code. It's not a program, but it's a little piece of code. Then I want to ask a question about it or I want to make a statement about it. And a statement I might make will be. Supposing X has type Int and Y has type float, then this little piece of code has type float and that's just like why. Well, because the programming language designer said so shut up.

MB: (laughs)

RG: But what's really sort of happening is then you've basically written a bunch of stuff and you've made like a statement. And this is sort of the. This is the language of the type system, it's like under a set of assumptions… this piece of code. Under a set of assumptions that are about the code and types, this piece of code has a type.

MB: Yeah.

RG: And then it's like, OK, so all that told me was syntax. Just basically we often in— at least informal programming languages or if you're writing down a specification of how types working in prose, you write things like that, you're like, yeah, like the type of this thing is this. And then there's like, well OK. So now I know how to— that's just parsing basically.

RG: So you can think of type checking as an extension of parsing, it's like parsing, but even worse.

MB: (laughs)

RG: Like not not only does it have to parse, but it has to pass all of these rules that say, like, we're going to say this thing has has type int and it's like, oh, and by the way, since your function takes an argument int, the first argument has to have type int. And the second argument has to have type float. Like you're only allowed to put expressions that I can say like this one has type int and and this one has to float. So it's OK to make this call.

MB: Yeah.

RG: So that's sort of the syntactic part of typing. So I say like just like programs have syntax type systems have a syntax and the syntax is basically what can I say about a small chunk of code, given a little bit of information about the surrounding context, which is often things about the variables that are in that expression.

MB: Type systems are programming languages within programming languages. That’s not going to make sense right now, but keep it in the back of your mind.

MB: Over time what I realized I was looking for when I asked about type systems was type checking. I wanted to know how to implement a type checker first, then bring on the mechanics of type inference and composite types and polymorphism and all that other stuff later. I needed to be more specific in my search. How does a type checker work?

MB: Of course this was not an easy thing to Google. Most of the blog posts I found start with formal logic behind types— vomiting out rows and rows of greek symbols without key or explanation—before getting to a code sample in a general programming language … if they got there at all.

MB: I ended up just reading source code. First pulling up a couple variations of Thorston Ball’s monkey that had type checking added to them. Then by digging into the internals of Go’s compiler.

MB: Each time I found myself looking at a recursive function walking the AST and subjecting each node to a set of conditionals.

MB: …..Is that all there is? You mean all these complicated looking formals with their fancy unexplained greek letters boil down to a bunch of if/else statements?

Stage 2: I realize that types are like formal specification

MB: On the surface of things types can seem like a very pedantic topic because many of us got our start programming in languages that use dynamic types and aren’t super strict about them. When that’s your reference point, caring about types can feel like caring about the Oxford comma. What’s the big deal if people don’t get it or don’t use it or use it wrong?

MB: But what I discovered while wading through all that information about type inference algorithms is that type systems actually create boundaries keeping the program from drifting into undefined behavior.

MB: Let’s say for example you want to evaluate the expression x = 10 / 4. Is the value of x 2 or is it 2.5? You can probably think of a programming languages where the answer is different. Maybe we’re working in one where 10 /4 is 2.5 …. is 10 +4 then 14.0?

MB: Why not?

MB: Floats and ints are handled differently inside the computer, so programs need to have clearly defined rules identifying what operations can be run on a piece of data and how to interpret what value comes out as a result. These rules are types. Without them it would be possible to push a program into unexpected and dangerous behavior.

MB: Type systems have several different kind of rules:

rules defining characteristics of each type
rules about what operations can be performed on each type
rules about what types come into functions and what types of values coming out of functions are
rules about how types relate to one another and whether conversion of one type to another is possible.

MB: All these rules should make a kind of proof tree, and that’s what powers type inference. A proof tree is a type of boolean logic. A set of true/false questions delivered in a certain order that prove whether— in this case— a variable of an unknown type has all the characteristics of a specific type.

MB: Okay cool…. so the type checker walks the tree and the if/else conditionals are checking whether a certain node follows the these rules …. but …. where are the rules themselves?

MB: I think the type checking part was the easiest part for me to understand, because having already gone through the construction of a parser and I'm like, OK, now I got my AST and like, being able to go, OK, this should be the same type. And if they're not or they're not like, OK, then we'll throw an error that that all makes sense.

MB: But then I got to the type inference part of things and like everything that I read was sort of documented in a kind of stuff that reminded me a lot of Prolog, which was like, OK, cool, yeah. That makes sense to me.

MB: But now I have absolutely no idea how to implement that within, like, a compiler. Right?

RG: Right, right. Right.

MB: Or even an evaluation loop. Like I don't want to like port Prolog into my programming language to write these rules down.

MB: Like how does the implementation of type inference, like really look like in the wild?

RG: Ok, so that’s… I'm going to first going to answer a different question than that.

MB:* Fair enough.

RG:* But for whatI hope is a good reason. And and what I'm hoping to do is leverage off of the idea of passing. Yeah. So when you learn because I in many ways I think of writing a type checker is writing a parser on steroids just because like type checking is like parsing but worse. So. When you write, like when you write a parser, typically you have like a grammar for your language and then nowadays you have a bunch of tools where it's like brica-brica-brica magic abstracts syntax tree pops out

MB: Yeah.

RG: But there's sort of another way of looking at this process in multiple steps, so one of them is that whenever you write a grammar for a language and I'm I'm just skipping the lexxing part, let's just make believe Lxexing was solved. So you have a grammar and it's got like a bunch of stuff. You can think of that as a. It's a really weird….. not weird, it's beautiful, but it's just a definition of a data structure.

MB: Yeah.

RG: And that's the parse tree. So the way the way I usually describe it is your parss tree is like every production on the left of like the arrow is— It's like a type and then every non terminal is a type and then every production is a different data structure and like a union type, basically, you're like, oh, it could be any of these three things.

RG: And then it references itself sometimes or it references somewhere else. You have this sort of tree structured data type, which can be like an arbitrary tree with a little bit of information. And the cool thing about that is that if you think about it that way, when you have a parss tree, usually what the way we think about parsing is, oh, give me a string of tokens and I will give you this parse tree. And the thing I like to think is you can think about this backwards. You can say, give me a parse tree and I will give you back the tokens that built it. Exactly. Like with nothing different. And so then parsing is just the process of running a program backwards, which is like like here's a set of tokens. I make believe that there exists a tree that produced the tokens. Your job is to give me the tree. And the amazing part is that you can often do this like it's like oh like I run it backwards. Like it's almost like, oh, somebody in their mind had an idea of the tree and then threw it out and all you have is the tokens, you know, like let's recover exactly the thing they were thinking about the notation and then it's too much garbage because there's like all this weird stuff you have to do in a grammar that like, oh, all these parentheses.

RG: I don't care that you have like seven like layers of parentheses around five plus nine. No one cares.

MB: Well we’re not writing a lisp here here. So we have fewer—

RG: I mean, like some people. Well, meaningless parentheses!

MB: Yeah.

RG: Unless you care about the parentheses, but it's like Python, some peculiar programmer who likes to always like I just really want to make sure that my precedent's is right. So I'm just going to add extra parentheses like nobody knows, like just tell me it's like five plus nine. We're good. So that's where you go from the parse tree to the abstract syntax tree.

RG: We're just like we're going to forget all the uninteresting details of how your program is written. And yeah, I can get you back a string of tokens, but it's not going to be exactly the same one, but it will mean the same thing. So I know this sounds like what does this have to do with type systems?

MB: It does it does. But I’m waiting for wait bated breath.

RG: So the thing that you saw that looked like prologue where you have like a horizontal bar, some stuff on top and stuff on the bottom?

MB: Yeah

RG: That is a grammar. It doesn't look like one, but it's a crazy grammar. And it describes a data structure which is what we would call a typing derivation tree.

MB: OK….

RG: So the way you can think of a typing derivation tree is it's like a data structure that has lots of extra annotations in it, like in a production compiler. What you would do is like, oh, I have an abstract syntax tree with a little bit of decorations, like I've got like an extra field called What's My Type? And then I stick things in it. This is worse. This is like we are going to just like stuff everything, everywhere. You're like, dude, you already told me that. It was an int, come on, you told me. Yes, I already know that the context is all of this stuff.

RG: So you can you can take all of those rules and you can write a data structure that captures it.

Stage 3: Type Systems are Programming Languages in Programming Languages

MB: The phrase data structure really threw me off because I could envision what that should look like and then couldn’t find it in code …. I was looking for a tree and couldn’t find any trees defining types.

MB: Then I found a slide deck from Princeton University’s COS 320: Compiling Techniques that walked through the various components of a type system bit by bit and it hit me.

MB: The if/else conditional are the tree. Proof trees for type systems are often described as a “grammar” but unlike the types of grammars used by parsers they don’t exist in a separate grammar file….. come to think of it, if you hand wrote your parser and lexer your grammar probably wouldn’t exist in a separate grammar file either.

MB: The conditionals are the tree.

MB: When I could finally see a type system with the boring, unsexy bits left in, I could see why Ron described it as a programming language inside a programming language. You start with a set of rules that define valid statements very much like a grammar. Then you write a function that parsers an AST and compares it to that grammar. And that function either throws an error or returns that AST with inferred types filled in or types converted as needed.

MB: It’s very much like foundation of the compiler itself.

MB: Ultimately, I want to keep Fault’s type system pretty simple. No composite types, no reassigning variables to different types then they’re declared as… I have to decide whether to change the grammar so that functions can specify what types the return … or I have to figure out how I want to do type inference. But the only way to answer those questions is to implement and see what problems I have.

MB: But the world of types is full of interesting ideas once you get the hang on them.

MB: So a lot of the papers that I have looked at that you've been involved with are about this thing called gradual types like what are gradual types exactly?

RG: Oh, yeah, OK. It's like, oh, dear.

RG: So gradual types is ….as broadly speaking, gradual typing is the idea that…. Type systems are really helpful, like they're type, they're spell checkers, they're grammar checkers, so they're wonderful that way. Type checkers are terrible, just like spell correction is on the phone. It makes my life miserable. So it's like simultaneously miserable and wonderful and especially in, like a large code base. It's really nice to have something that gives you some guard and sometimes doesn't get in your way. So the research that that I've done on this is the idea that it would be nice to have like some code that's got these type checks in it and they mean something. They say like if you give me certain kinds of data, I will produce certain kinds of data and it goes even further. It's I am expecting you to give me certain kinds of data. And if you don't, you're you like bad things. Don't do that because it'll be hard to understand my code. I'm understanding this chunk of code on the basis of what kinds of inputs I'm expecting and what kinds of outputs I'm going to produce. And you've got this other piece of code, which is like, yeah, I made no commitments.

RG: So it it's useful to be able to protect this piece of code so that whoever's programming it when they're on the inside, they can say it's not my job to worry about what nonsense other people are going to throw at me as long as I've stated my my conditions for use and the promises that I'm going to do— the things I promise if you meet my demands.

Syntax Sugar (featuring James Houghton)

Marianne — Wed, 10 Mar 2021 03:53:02 +0000

Summary

A few weeks of user testing has revealed specific problems with the syntax of Fault. Marianne ponders various approaches to solving those problems and talks to James Houghton about the intersection between programming and system dynamic modeling.

Links

Rosetta Code
JamesPHoughton.com
PySD a cross compiler and simulation engine that translates models created in Vensim to python

Bonus Content

Become a patron to support this project.

Transcript

MB: Oh boy…….

MB: I’m back.

MB: It took me longer than I thought it would to finish user testing the pre-pre-pre alpha version of Fault. Partly that was scheduling. Partly that was wrestling with design issues highlighted by the user testing itself.

MB: But that’s good because that was the whole point.

MB: I conducted two different types of user testing. The first was passive. I logged every time someone used the repl-- just logging the spec before parsing it. About 50% of people just ran an example model without any changes, just to see what the code looked like and what the output was.

MB: 20% then ran the same model again with a minor tweak— usually changes a single value and seeing what the difference was.

MB: Only a few people attempted to build their own models. One person decided to lint an example model, keeping the significant values the same but removing whitespace in certain areas.

MB: This data was useful and will continue to be useful in its own way.

MB: The second type of testing was pairing with people who volunteered and either writing a model or going through the documentation with them and asking them questions about how they expected pieces of code to behave. This was really useful but sometimes frustrating because I often wanted to put different options in front of them and say “well how about this?” but for a lot of the issues they raised I did not actually have a good alternative available.

MB: I got what I needed out of the conversations but I couldn’t help feeling like I could have been better prepared.

MB: The first problem that—truth be told bugged me a little going into the tests and continued to bug me more and more every time it was mentioned is the required parameters of the stock/flow objects.

MB: If you recall: you must define a name and value with a stock and a function with a flow. But in the same key-value block you can also define any normal of custom properties. There are different rules for these special properties with their reserved keywords and the user defined properties. And sometimes special behaviors. Functions can be initialized with a starting value so that you can reference historical outputs of the function— one person used this to write a Fibonacci sequence in Fault, but you shouldn’t do that with a flow’s default function.

MB: A precedent— a special, non-required property of flows— must have a int value. A name property of a stock must return a string somehow.

MB: I told myself going into testing that all languages have special reserved keywords and builtin functions with specific parameters. But the more I worked with people interacting with the language for the first time …. the more it felt clumsy and brittle.

MB: In the case of flows and their default functions this created a weirdly redundant syntax. Okay we want a reserved keyword to represent the flow’s function …. “fn” for function seems logical. But oh…. since functions themselves are declared with the word ‘func’ followed by a set of curly braces… that means…..

User1: When I saw FN and then function, I was like, oh, that's function and that means function.

MB: Yeah.

User1: So I don't know, is this sort of like a key value pair or is this I mean, this is the function and this is the property?

MB: Yeah, and this is this is like touching on like one of the things I've been exploring, kind of like meditating about.

User2: The input flow then is taking as a target the queue and its function again function seem special here. That’s another one of my notes. If flows always have a function like is this a keyword really? Or are there other function names or what's the … thought here?

MB: Yeah…. for sure

MB: I need to figure out how to simplify things. Its true all languages have these little quirks, but typically they develop those quirks overtime as they change direction and attempt to maintain backwards compatibility. It’s seems stupid to start off with so many quirks from the beginning.

MB: Then another problem I picked up while preparing to run test exercise themselves. If you opted to write a model the task I would suggest is modeling a message queue. There are a couple of ways you could approach thinking about a message queue as stocks and flows. You could think about the number of consumers and the number of publishers as stocks. Or you could think about the messages themselves as a stock and the movement of messages from a queue to either sent or a retry queue as a flow.

MB: Except…. how do you change which stock the flow is sending data to? There’s certainly conditional logic in Fault, that part is easy, but the flow has one source and one target stock maximum. With no side effects.

MB: So you either change the flow target stock dynamically or you have to build a way more complicated model that doesn’t really map well to the behavior you’re trying to represent. You end up painting yourself into a corner.

User2: So then producers have value, this is another thing I noted here to talk about… value seems to be special. It's definitely special within the repl, but is it special overall is is my question. It also seems to be special overall because of the way target and source work, because they implicitly change that dot value value.

MB: Yeah…. So this is something I've been going back and forth on rather regularly, basically the idea of can you assign— how do you do assignment as the output of a function? Right. So effectively, the function of a flow assigns values to the value property of the stock it's connected to, but doesn't have to be that way. Right?

MB: And there are various places where, as I'm trying to work through models for my own tests, I think like, oh God, it would be so easier if the flow could send this value over here and this value over here. So I could definitely like with some fairly minimal retooling, develop the syntax and the logic to sort of say, like this value gets sent over here and it's now assigned to this part of the stock and this value gets sent over here and assigned to this part of the stock.

MB: The thing that keeps me from doing that is kind of not wanting to move away from these very tight, pure functions that only really do one thing, or change one thing. Right? So that's the part where I'm like trying to figure out how much utility do I get from giving that level of flexibility where it's like it's not like it's not necessarily value that's changing.

MB: You can have the function of flow, change other things, and therefore build more complex and lighter rate models versus adding a level of like. State change chaos to the overall model, right, because you are— It is a bounded model, but it is still potentially, as the model grows more and more complicated, it gets more and more computationally complex.

MB: So I’m still struggling with that. I think what I will probably end up doing is testing out that kind of delegation and seeing how I like it and then maybe running some more tests with people and seeing what kind of chaos it opens up if we try to build a really big model. But yeah, so noted for that. So that's really why Value is this special thing that doesn't behave quite the way the other properties behave

MB: Then on top of that Fault tries to draw conclusions about what you want it to do with the value produced by the flow that in retrospect might have been confusing.

User2: The source is the queue size that is now that consumers.

Yeah, and that the.

User2: Yeah, and that the….They're going nowhere, so I want to create a new value which goes from zero, this is kind of related.

User2: Yeah, I guess the new value goes from zero, even though it's got no target. Is that the right way to think about it or?

MB: Yeah….

User2: It's always a constant zero?

MB: if there is a source value and not a target value, it will essentially treat the source as if it is the target value. It's just at this point, it's just syntax to make it clear for people's heads rather than like what the code is doing. Right? If there's only one stock it's connected to, it will do the same thing. No matter if it's targeted at the source, it only changes its behavior when there are two stocks on either side. I see.

User2: I see. I didn't didn't realize that because it feels like sources being subtracted from the targets being pulled.

MB: That is, of course, the idea of it. But if you were to connect the flow to a stock as a source, but the output of the function was a greater number than the the source like incremented the source, it would just increment the source. It wouldn't go, hey, wait a minute, this is supposed to subtraction. This is flowing out. I just did not seem worthwhile to do that, picking you in about it. But it did seem worthwhile to sort of help people, people with. So to think about it in terms of this is the source and this is a flow out of the source and to be able to allow them to define it that way if they so wished.

MB: Okay…. what to do about this. Well first, if I allow the function to explicitly assign values to stocks then having special keywords for source target and value is unnecessary. You can declare a flow with stocks assigned any key name you like and change whatever property of that stock you need to. That one change adds a tons of expressiveness and eliminates three out of three out of our five reserved keyword.

MB: The stock name itself is unnecessary because the statement where you declare it already gives it an identifier. 4 down….

MB: That leaves the function-function problem. It took me a loooooooooooooooooong time to figure this one out. Sure I could make the reserved word something like “rate” and eliminate the ugliness of the repetition, but that isn’t really satisfying. It’s still a special property with slightly different behavior than identical looking properties elsewhere.

MB: I spent a lot of time pondering different ways of arranging blocks of code to separate out this one special thing in such a way that its different behavior could be anticipated. I spent a lot of time on Rosetta Code looking at different syntax from different languages hoping for inspiration.

MB: (If you’re unfamiliar with Rosetta Code it’s a great site displays versions of the same simple programs in different languages side by side. An amazing resource if you want to think deeply about design patterns in programming language grammars.)

MB: Then suddenly, while doing something else the answer hit me. And it was one of those situaitons where once I thought of it I was shocked it took me so long to think of it.

MB: The reason why the function-function block seemed necessary is because Fault had no syntax for call expressions. When the model runs it needs to know what functions it’s executing. I was using a special keyword to determine that, and then adding additional special optional keywords like delay and precedent to configure what the model does as it runs through a single step. All that logic is abstracted away from the user and the special keywords expose those configuration options.

MB: …..Why on earth was I doing that? These are programmers right? Why don’t I just let them program what the model does in a single step?

MB: …………Yeah. It’s obvious right?

MB: So in addition to changing flows to allow them to assign values to any number of different stocks. I added something I’m calling a run block.

MB: At the end of every model is an optional configuration statement that reads for x run all; I say optional because if you remove that line or never add it in the first place it executes all your flows in a five step model by default. But if you change the statement you can make Fault run part of the model or run as many steps as you like.

MB: Now instead of run all, the proper syntax will be run curly braces followed by a definition of what is happening in each step. Now if you want to write a delay you just write a delay as a conditional in that block. If you want to change the order flow execute, you change lines of code in that block. And you can call the function in the flow object whatever you like because you call the function from that run block.

MB: Of course the trade off is that you can produce something in Fault that is not a true stock/flow model if you want… but maybe that’s not as damning I would have assumed.

MB: In my user tests I spent a lot of time talking to programmers of various skill levels, but there was one other group I wanted to chat with….. people who write system dynamic models.

MB: A few weeks ago I sat down with James How-tan a researcher at the University of Pennsylvanian who teaches college students how to build models and also has created a suite of tools to run those models in python.

MB: So I always thought of ASD is like being almost niche to the stock flow abstractions. Yeah, but it sounds like for you it is broadly modeling these kind of social dynamics as a whole.

JH: Yeah. You know, you have human actors with behavioral realistic decision roles that are interacting to create some some phenomena that doesn't exist in the individuals themselves.

MB: So that being said, how do you pick, you know, your model constructs like how do you decide this fits best with an agent base, Stock/Flow based, This fits best with some other construct.

JH: Yeah, there's two sort of tools that you can use for thinking about that.

JH: One is the level of aggregation of the model or its scope, like what do I want to stick in the model and what are the boundaries and the other. So that's sort of like capping a top line on on the scope of the model. And the other thing you want to think about is the granularity of the that you want to represent. And so in this case, I needed to get the granularity all the way down to the level of not just the individuals, but the individual beliefs within the individuals. And so for me, that made it a an agent based model. But I have a very good friend who is modeling the current epidemic and his models are compartmental because the questions that he's asking are more at the top level about the society as a whole. And so in that case, you can create these aggregations, the stocks of individuals and represent these groups of people as a single number.

MB: This is so fun because this is weirdly intersecting with something else I'm doing in my work environment around programmers intent, because I think the the core issue with sophistication on the technical side is that you are never going to write a specification that is 100 percent accurate to every every conceivable factor in a system. Right. So at some point, you have to make a decision of the level of detail. Yeah, but that always drives computer people crazy because they want absolute truth. And they like this idea that I can write the spec and I can prove that it's correct and that's objective, not subjective. And so there's this question of like, how do you reliably set those boundaries of like what level of detail you need? So connecting it to. Well, what research questions are you asking them to model?

JH: Yeah.

MB: It makes a lot of sense. But it's also not an answer that my community, people like because they want to share models and reuse them and build on top of them. And it's like your research questions are not in line with somebody else's research questions. You can't reuse their work, right?

JH: Yeah, well, I think the most important thing in modeling and probably in academia as a whole is to really know what question you're asking.

MB: Yeah.

JH: And when I read an academic paper that doesn't really hang together and I can't understand what it's saying often the reason is that the question isn't clearly articulated and possibly isn't clearly understood by the authors. And the same is true when you look at a model and if it has a whole bunch of pieces and you're not really sure why they're there, maybe the reason is that it was unclear why this model is being built.

MB: Yeah.

JH: And so the best models are the ones where you can really clearly articulate exactly what the research question is.

MB: Sometimes I think there’s a certain magic to having specific conversations at specific times. I don’t always work on this project as diligently as I could (another secret reason why it took me a bit longer to finish user testing than I thought it would) I feel like I have to sit with things sometimes … waiting … not exactly for inspiration but for …. something.

MB: As it happened I procrastinated on reaching out to James for oh … about a month. I don’t know why, I just kept putting it off. And as luck would have it by the time I did reach out I was in the middle of exploring approaches to capturing programmer’s intent for a completely different reason. Right now at work I’m working with a team to build new technology, but of course I’m coming from a career of slaying dragons of tech debt on existing systems. Naturally I can’t build a new system without thinking about how functionality will drift over time, how documentation will fall out of date, how more and more lines of code will make it harder and harder to onboard new engineers. There’s some interesting research work around formalizing programmer’s intent into the code and some theoretical work around compilers that can identify when a function violates the programmer’s stated intent.

MB: Had I not waited, these comments in this conversation probably would not have stood out to me the way they did, and that’s a stroke of luck because I think they reflect something critical about Fault’s design that I hadn’t put much thought into: a model’s scope and assumptions are defined by it’s research question. Ergo the thing that a spec has to communicate most clearly is not how the thigh bone connects to the leg bone but what the intention of the model is.

MB: Assertion have been a part of Fault’s grammar from the beginning, but I was mainly thinking about them in terms of simple boolean statements like x > 5. Yet just as it is my habit to read the unit tests first when trying to figure out a new code base, these assertions will broadcast information about the programmer’s intent. It’s going to be important to invest some time and energy into figuring out how to emphasize their significance.

MB: Something that came up in our chat that genuinely surprised me is how from James perspective the characteristics of visual programming compiling to code wasn’t just a crutch for silly non-technical people. His tools don’t convert to python to remove the proprietary software used to build the models. He wants to keep that drag and drop stock and flow diagramming stage.

MB: This caught me off guard because I find being given a visual abstraction and maps to autogenerated code frustrating. I’d much rather open up the hood and write the code directly.

JH: The thing is, the stock flu models, the diagrams themselves are actually… think about it like a technology in a way, in that this is a tool that we can use to think about the structure of systems. So everything that's represented in that stock flow diagram is just something you could represent with math if you wanted to. But by structuring it with the stock and flow diagrams in the feedback loops, you see the structure of the system in ways that you don't see when you just have lines of code on the screen. So mathematically they're equivalent. But in terms of your understanding of the system, you do a lot better when you have the visuals.

MB: Is the value of these tools actually the visual? I'm sort of approaching it probably too much as a programmer and seeing the value of the tools being the interface of code, basically giving you shortcuts, right? Where it's like, OK, this understands what a stock is, understands what the flow is and like makes it easier. You have less code to write because there are some built in like syntactic sugar that makes it easier to get into that place and then when I actually look at the code. I'm like, no, this is just… like you could do this in any (programming) language.

JH: Absolutely.

MB: Is it really like the visualization and like maybe some graphing is the why these tools are popular?

JH: It is, exactly.

JH: And and and these diagrams are a tool for thinking about the structures of complex systems. Once you have them built, you can translate them to any language you want and the math will work just the same.

MB: The programmer in me stubbornly insists that I can probably understand a system better from looking at code…. and yet … reading code is so much harder than writing it. Perhaps visualizations do make it easier to communicate general information about a system.

JH: The the writing down of the equations is the easy part. Honestly, the the understanding, the structure of the system well enough that you can write down equations that accurately represent it is really difficult.

MB: Yeah.

JH: And what's dangerous is that it doesn't look difficult.

MB: Yeah!

JH: When it's done well, it becomes really clean and and and easy to understand. And that's when you know that a real master has been doing their craft, there.

MB: So okay…. I have a few more design questions that I need to develop answers to before this journey is over.

I need to figure out how best to present assertions so that they are treated both as tests but also as a documentation of the programmer’s intent.
I need to figure out how to incorporate visualizations into Fault’s output. The prototype would generate a dotviz flow chart before running your model and I found that to be really helpful. I still don’t like programming via visual methods, but when I’m building Alloy models the ability to check what Alloy thinks my system looks like is often the best debugging tool.
In general I need to think about how a person interacts with and understands a spec someone else has written and how the code arrangement makes that easier too harder.

Then there was another key challenge that this conversation highlighted:

MB: What are the common mistakes people make when they're building models?

JH: There's a lot of things.

JH: I’d say the biggest ones are not really being specific about what they mean by their their stocks and flows, so that that's in some ways it's a conceptual sloppiness where you haven't gotten all the way down to what is it you really, really, really mean here.

MB: Yeah.

JH: And then there are just some mathematical mistakes that are easy to do. Or, you know, an obvious one is that if you have a stock with an outflow, and the stock is something that, like water in a bathtub, can't really go negative. You need to go to check that it hasn't gone negative. And so what you need is a feedback between the level of the stock and the outflow. And so we'll call it a first order control on the outflow so that you you don't go negative when you shouldn't. And if you forget that, it'll work most of the time until you get to an edge case where your stock has gone negative and you didn't notice. And then all of a sudden you get really, really strange behavior.

MB: So, like, I almost like instinctually want to think about this as a type system issue. Right?

MB: Like, if you have a particular stock that cannot go negative, that's something that can be reasoned about through type systems. You could sort of say this is a this is this is a characteristic of this type that it never is negative and then possibly reason about it on the compiler or the runtime with that thinking in mind. Like, this is the problem with mixing multiple interests, they collide in strange ways sometimes.

JH: This is the power of mixing multiple interests!

MB: laughs….. perhaps, we'll see.

User Research for Programming Languages (featuring Michael Coblenz)

Marianne — Wed, 23 Dec 2020 04:25:40 +0000

Summary

Marianne has a working prototype of Fault, but still no idea if anyone will understand the design or find it useful. She needs to test it with some users and see whether it has the right features and syntax. To do this she talks with programming language researcher Michael Coblenz, who specializes in techniques for testing usability of programming languages.

Links

Marianne’s DevOpsDays Talk
Interdisciplinary Programming Language Design
Coblenz’s user research on type systems
More about Michael Coblenz
Jetbrains MPS
XText

Bonus Content

Become a patron to support this project.

Fault User Research

Open to helping Marianne out by giving up 30 minutes of your time to try to use her language? Book a time slot here

Too shy to talk to Marianne directly? You can play around with the Fault prototype at fault-lang.herokuapp.com

Transcript

MB: Back when I started gathering research trying to figure out what I wanted to do and how I was going to do it I came across a paper titled: Interdisciplinary programming language design, all about how program language design should include more user research.

MB: User research for text based interfaces has been a particular crusade of mine for a while. Two years ago I gave a talk about this topic as it applies to SRE and DevOps teams at DevOps Days DC

MB: And so when you have unexpected user behavior, like one of two things tends to be the result. Either the system or the product that they're using doesn't know what they want to do and gives them an error that may be decipherable or may not be decipherable or… it seems to work. And it can be difficult to sort of see where your preferences should be as a software engineer because, like, errors are super annoying and they frustrate users and they make them mad and then they complain about your product or they may be stopped using it.

MB: But if it works and it's unexpected that we don't actually know what the system is doing in response to that command, maybe it's doing the right thing. Maybe it's doing something else. And if users are using your systems in ways that you didn't anticipate, then it's going to change your scaling needs ultimately, which will ultimately change how you monitor for those scaling needs.

MB: So really important concept about why design is relevant for people like us who mainly stay on the back end of things. Is that design determines how people use things and how they use it determines how you have to scale it when you have to scale it and what you're scaling when you're scaling.

MB: It went really well and I still have people come up to chat about it from time to time so I’m really proud of that.

MB: Anyway, despite my passion for user research, I had not given much thought to how user research fits with program language design. But as I develop my language…. I keep comforting over and over again the reality that I don’t actually know what inputs I should be expecting because I don’t actually know whether my ideal design makes sense to anyone else.

MB: Sure…. I could probably come up with a list of expected and illegal variations…. but writing the scaffolding to catch such behaviors, stop undesirable activity and communicate the problem back to the user is…. well…. a bit tedious. Error handling certainly isn’t the MOST fun part of writing a language. And I could be missing something big too.

MB: I’ve always felt that the biggest reason why other specification languages have failed to catch on is because it is not immediately obvious to the average programmer what you should be doing.

MB: I’m definitely sold on user research for language design as a concept…. but …. a programming language is much more robust than a command line tool and has many more conditional branches than a graphical interface. I needed some advice on how exactly to do this, so I had no choice but to track down the paper’s author.

MC: I'm Michael Coblenz. I recently finished my PhD at Carnegie Mellon. My work is on the usability of programming languages. So the general question is how do we design programming languages that make programmers and software engineers more effective at achieving their goals?

MB: This is what all forms of design have in common: it’s all about goals, not some universal standard of code quality. I approach legacy modernization in the same way: let’s not focus on what’s new and “better”, let’s focus on what the system is supposed to be doing and what’s the best way to do that.

MB: In that line of work, when you think of things in that way … you end up turning off fewer mainframes and getting rid of fewer Excel spreadsheets than I assume you will.

MB: But I digress….

MB: So I'm really familiar with user research from the product perspective, right? I'm building a website. I want to make sure that the usability of the website is as best as it possibly can be. So I'm going to take some paper prototypes. I'm going to take some wireframes and sit down with some users. How is your research for programming languages is different?

MC: Right. So it's different on a variety of ways. One of them is that typically you expect your users to be experienced in various ways, now not necessarily, right? Some programming languages are targeted specifically at novices, you know, beginning programmers. And so you want people to be able to write software even though they don't have much, you know, computer science background. I tend to focus on programming languages that are more for larger scale systems. And so I tend to think more about how can we prevent bugs and systems. And so the usual ways you prevent bugs and systems are by various kinds of type system approaches, which may make the system harder to use. And so there's this kind of interplay between how you train people, what you teach people, what experience they have and what behavior you see when you actually get people to use your system.

MB: That's the thing that I think I am trying to wrap my mind around is that there is a certain amount of learning that we expect people to do when they're picking up a programming language. So how do you separate poor usability from no, that's just the learning curve with this language? Like how do you level set?

MC: Yeah, I wish there were a good answer to that question. There isn't really yet. You know that’s why it's still research in part. I have some answers. Right. One answer is, if you can build something that you can show is effective, then you have done well enough. Another answer is there's no reason to build something that's harder to learn or harder to use than necessary. Right? So if you teach people something and then you have them use the tool you taught and then you discover that they had problems, if you can address those problems, well, you're making their life better.

MB: Hmm.

MC: Right? So why not do that?

MB: Hmm.

MC: So, you know, then the question is, OK, you know, are you only improving your improving learnability or are you also improving kind of long term performance?

MC: And you have to kind of think more is theoretically about that. Are you going to make it annoying in the long term? And. There are lots of you know, we have larger scale tech links like case studies where we can kind of think about that. So it's important to kind of see both sides of the picture.

MB: Hmm. And like what kind of techniques to use when you're doing your research on a programming language?

MC: Yeah. So I've gotten kind of traditional user studies. So I give people programming tasks before I actually before I give them the tasks, I give them some training materials to teach them the language.

MC: And then I try to see what problems they encounter and then try to figure out, OK, why are they encountering these problems and can I change the language or possibly the documentation in order to address those problems?

MB: Okay so what should I expect people to know before they pick up my language and try to use it?

MB: I supposed an understanding of basic stock/flow style models would be necessary, but that is a simple enough concept to communicate reasonably well through documentation.

MB: I would also expect them to recognize the syntax around object properties because that’s the way I want to represent stocks and flows. And while we’re at it the basic syntax around anonymous functions too.

MB: The first user tests therefore should seek to optimize how that information is communicated and test whether users create models that make sense given those patterns.

MB: Most of that can be done with a text editor, or paper. Sketching out how models should look and writing out a representation in the syntax of my language … but eventually I have to comfort the reality that I need to build something interactive to actually test its usability.

MB: Do I have to build a working language to put in front of users? Fortunately, Coblenz had a solution for that issue.

MC: So one of the problems we have in programming languages is design and implementation is very expensive. It could take months or years to design and implement a programming language, even even just sort of the core parts of the language. Never mind the library or tools, never mind all the things need to actually be created in the language. And so, you know, you could spend years of your life building things and then discover that they're no good. Right? So the idea is, can we retrofit our ideas into existing languages or assimilate them without having to implement them completely.

MB: Okay so… I can use my grammar to generate a parser and insert some additional functionality into another language. My ANTLR reference book showed me how to parse and generate code in a language called dot, which has a javascript library that can rendering simple flow chart style visualizations. That sounds perfect. The first implementation of my language will actually be a transpiler, taking a spec and transforming it into dot code so that the user can visualize the connections between stocks and flows.

MB: That kind of test feels like it can be open to anyone on the internet. Most of the work stays in the browser…. and maybe when the user finishes their model and clicks a button to render the visualization, the browser sends a copy of the model to a server where I can track what types of models people are trying to build.

MB: But none of that simulates the behavior of the language itself, right? I need some better ideas about how you do that. How you simulate the behavior of a language without building the language.

MC: I was designing a language called Obsidian, and I had some ideas for a type system, but I wanted to know, can people actually work effectively with this type system? Right. So I took some of those ideas and I inserted them into Java. And then by which I mean, I told people that I inserted them into Java, but I didn't actually implement a type checker. Right? And then I said, OK, please do these programming tasks. And any time you want to compile, let me know and I'll see if there are any compilers. Right?

MC: And so as the experimenter, I can tell them verbally, you know, error on line forty-two you're losing ownership of this asset here. And then I can see, you know, does that error message make any sense to them? Can they make progress along the lines that they're supposed to make progress on for this task or are they stuck? And if they're stuck, then what information do they need to get unstuck? How do I kind of clarify the system or refine the system design in order to prevent people from getting stuck in this way?

MC: And then once I had done that, then I actually built the system.

MB: That… that feels to me like very— I find that very intense, the thought of doing that, because I feel like you have to learn and anticipate what the common mistakes are likely to be made with the language. And like how a type system would interact, how it would error if given that that endpoint. But like, what did you do to prepare for that?

MC: So I spent a lot of time designing kind of language prototypes and so I had a pretty good idea of what the type system would be able to do and what it couldn't do. Yeah, you have to have a you have to have the idea in mind in order to kind of provide a good simulation.

MB: Right. You have to really thoroughly explore and know it before you can really…

MC: Yeah. Well, I mean, you do kind of theoretical work to try to figure out what is this thing that I'm building and what are its properties. And you don't have to do a perfect job. Right, if you. If you give sort of inappropriately good error messages and the thing works out, then, OK, you're going to try again with a more refined prototype or more accurate error messages. On the other hand, if people can't make progress, even with your really good error messages, that it means you need to rethink things.

MB: I don’t feel prepared to predict what kinds of compiler errors a compiler I have not built will throw. I have never built any kind of compiler … I have never even looked at the code for a compiler before.

MB: But the first step in any iterative cycle is figuring out what the minimum viable implementation is … and of the functionality I’m looking at, maybe that’s the behavior of a flow.

MB: If a flow is a pure function … the types of errors that one might encounter doesn’t feel too intimidating. There are scope issues, is a given input visible to the function? Assignment issues. Basic arithmetic issues … Some potential type issues but very limited ones. There’s no reason is use a variable that isn’t numeric in a flow.

MB: My first attempt at building something that mocked execution for user testing I don’t like very much. I walked the tree and rewrote the functions as strings of javascript code … basically the same thing I did for the visualizations but a whole lot more complicated.

MB: I mean it works. It runs and it runs my models correctly. But the idea of it was to kind of do a pseudo transformation to javascript and execute that and it ended up being a mess of eval statements that feels gross and will probably break real easy.

MB: But building it did help me refine my grammar a bit— which was useful— and I had to shake off my anxieties about working with a stack.

MB: Most languages execute from the tree created by the parser by pushing values onto a stack and popping them off. You follow the tree all the way down, store the value of the last node on the stack, then as you work your way back up you take that value, insert it into its proper place in expression in the node above it, evaluate the expression, and push the result onto the stack. The node above that takes that value off the stack, inserts it into its expression, evaluates that and puts that value onto the stack. And so on until you get back to the top…

MB: This was one of those concepts that made sense to me but that I was nervous about doing wrong… it felt like something where I could make a basic mistake and not notice or not realize it. Like I could pop off and assign the values in the wrong order.

MB: Anyway it was great to push myself to just write the code and realize that— yes in fact the resulting program’s output was what I expected it to be…. But I knew I could do better. Once I got over my nervousness about using a stack that way it seemed silly to write strings rather than just evaluate the expressions in the tree.

MB: So my first functional implementation of my language will be a functional implementation of my language…. now what should I do with it?

MB: How scientific are your user research sessions, because like at least for the product framework thing, my experience has always been that they seem to be very heavily anecdotal and that's useful, like just sitting in front of a user and like seeing they're making observations about their experiences often enough to bring something back for iteration, whereas something like human computer interaction research seems to be much more structured and scientific with like control groups and all of that. So where would you recommend on that range? Is it necessary to go all the way to the control group side, or is there value in anecdotal or is there some middle ground that we should stick to?

MC: Right. So. You can evaluate the sausage very carefully without being very careful about how you made it

MB: (laughs)

MC: Right? Or you can think very carefully about how to make it. Or right, so when you use user centered design methods, you get a bunch of where you can get a bunch of feedback from users or via users about… design prototypes that you came up with that didn't work and why they didn't work. And then you feed those back in to your design process to make a better design and you keep doing this and eventually come up with design that you think is pretty good. And then you want to know, OK, is it better than something that already exists? I mean, is this you know, if I actually achieved something?

MB: Yeah.

MC: Or have I been kind of spinning my wheels and not made any progress? So at that point you can do an empirical study to do a comparison between the thing that you created and some earlier thing that you maybe started with or you're comparing to. And so. So that's a scientific evaluation process. And then maybe I should say an empirical evaluation process. But then the question is, OK, I did a bunch of work to refine that design. And to what extent does that work generalizable. That kind of gets to what extent is the scientific you know, to what extent have I learned generalizable knowledge that other people might be able to apply? And it's hard to know in the moment. Right, so you discover people have some problem with some design approach that you had and then you refine your design and they don't have a problem anymore. So does that mean that if somebody else makes a similar design decision, they're going to encounter the same design problem that you did?

MC: That's not clear, right, so, you know.

MC: How you generalize from these studies is not necessarily clear in the formative part, one of the things that we do is we ask people afterward for their opinions and you can try to glean from some of that, you know, what parts of the system work for them and what parts of the system didn't work for them. Yeah, I think there's an ongoing discussion about. You know what, parts of this will generalize, but parts don't.

MB: I don’t know that I caught on to his point about science being generalizable until I listened to our conversation again. It really highlights for me the idea of goals. What are our goals?

MB: About the same time I had this conversation I started learning about these things called language workbenches. They’re tools to build domain specific languages. While ANTLR and bison and other tools will generate parsers from a grammar, workbenches will generate almost everything— parsers, linters, IDE integrations, a whole language in a box.

MB: (FYI If you want to check this out the two tools that seem the most mature are Jetbrains MPS and an Eclipse tool called XText)

MB: When I saw these tools for building languages I couldn’t help thinking to myself, shit…. am I going about this the wrong way? But then I realized that …. so far, I’ve built and rebuilt elements of this language several times in different ways. The first time I build something “from scratch”, the next few times I’ll use more advanced tooling and boilerplates … each time I build it I have a different experience and learn different things.

MB: And by the same token, each type of user research— from the very simple just talking to people to the very structured control group study— each type will illuminate something different. So it really all comes down to goals. If I just wanted to build a language I could load the grammar into a workbench and throw my nice generated code online … but I do want to understand how these things work, and I do want to build something that people will actually use to model things.

MB: So I have to just keep iterating until I accomplish those goals.

MB:How do you find your users in general?

MC: Yeah, so this is always a challenge. You know, I did that work at a university. So at a university, it's easy to get access to students.

MB: You put up the flyer with the little like tabs. Please come and we'll pay you twenty five dollars to program a computer sort of thing?

MC: Yeah… did some of that. Emails to degree programs, that's a really good way because then you get students who are in the right programs, like for example, we had a masters of software engineering program.

MC: And so a lot of those people had some industrial experience.

MC: And there's some evidence that a lot of the practicing software engineers have somewhere in the industry have somewhere between zero and five years of experience in the industry. So if you get people in an MSA program who are generally either right out of undergrad or a few years out, there's an argument that that kind of reflects a significant, significant fraction of, you know, the developer workforce.

MC: It obviously does not reflect all of it. So there are other people that, you know, at companies who have kind of easier access to those kinds of users. And a lot of people are doing that work too, you know, recruiting via the Internet, collaborating with industrial partners, that kind of thing.

MB: You’ve been listening to Marianne Writes a Programming Language. So I’m going to take a break for a few weeks while I do user testing and some more research— as fun as the stream of consciousness episodes are I very much prefer to know what the hell I’m talking about (mostly)

MB: BUT! The prototype that I talked about this episode… that’s online. If you’re down for doing a little passive user testing you can play with the pre-alpha version of Fault by going to Fault-lang.herokuapp.com. That’s (F-A-U-L-T dash L-A-N-G)

Exceptions Are Not Errors (featuring Smokey Jones)

Marianne — Wed, 16 Dec 2020 04:28:27 +0000

Summary

Inevitably the best way to make design decisions is to practice implementation over and over again. Marianne experiments with writing different types of specs and considers various ways they could be executed under the hood. Midway through she realizes she doesn't actually understand how to think about errors and attempts to do more research while her cat tries to distract her.

Links

Thinking in Systems
Insightmaker
Introduction to System Dynamics Modeling with DYNAMO
Null References: The Billion Dollar Mistake - Tony Hoare

Bonus Content

Become a patron to support this project.

Fault User Research

Open to helping Marianne out by giving up 30 minutes of your time to try to use her language? Book a time slot here

Transcript

MB: In trying to figure out what my language should look like and how it should align itself philosophically, I spent a lot of time writing sample models in Go.

MB: ...This week my guest is (unfortunately) my cat, Smokey Jones.

MB: I'm actually surprised I haven't had a need to introduce you to him before this. Interrupting conference calls is sort of his thing. Knock it off!

MB: Anyway...

MB: The type of modeling I like to do is called system dynamic modeling. If you've reading the book Thinking in Systems, you're probably already familiar with the terminology I'm about to explain. I prefer these models over more traditional specifications and verification approaches because I'm interest is in resilience. Perfect systems that never misbehavior do not exist. I'm much more interested in systems that can absorb a multitude of errors before losing their integrity.

MB: In system dynamic modeling you have stocks and flows. A stock is a resource of a certain amount. A flow is the rate of change of that resource. The traditional example is a bathtub full of water. The water is a stock. The rate at which it flows out when you unplugged the drain is a flow. The rate at which new water flows into the tub if you turn on the facet is also a flow.

MB: From these two building blocks, we can model almost any type of system. My equivalent of a "hello world" is modeling a load balancer. I have a stock representing the amount of memory for each VM and a flow representing traffic consuming that memory. The functions that govern's the flow's rate can product a round robin affect, or turn off and on depending on the value of each VM's stock.

MB: A model in this sense is a series of feedback loops. All you really need is stocks and flows, but for convenience we might include some additional elements: delays (which involve how quickly or how often the flow operates) and what I'm going to call factors which will operate a bit like constants. For example, the number of workers in a factory obviously has an effect on how quickly new product is produced. Whether that effect is positive—more workers mean more productivity— or negative—more workers mean slower production—depends on your philosophy about the issue.

MB: Up to this point I've spent a lot of time reading and picking the brains of other people much smarter than me. I can't go any further until I make a few design decisions about this language.

MB: I want to represent both stocks and flow as structs. Stocks will have a name property and a value property. Flows will have a delay property, a target property linking it to a stock, and a rate property.

MB: What data types should I allow? I want to keep things as simple as possible to start out. Strings are an obvious one. Integers another must have. I'd love to get away without floats, but that doesn't seem likely. At this point I'm not even sure I need an array. The language is going to use them under the hood of course, but allowing the user to create arrays seems like it might add unnecessary complexity.

MB: Oh well, early days still… can always change that later.

MB: Throughout this process I've been using what's come before as a reference. I spent a fair amount of time picking through the source code for Insightmaker (an online tool for system modeling... thank God for open source~~!) but my favorite resource has been my copy of Introduction to System Dynamics Modeling with DYNAMO. DYNAMO was a language written in the 1950s for simulations on mainframes. It's a product of its era, at first glance it's a jarring jumble of all caps commands and creative uses of columns. When I see the code for these models the part of my brain that knows a little COBOL kicks into gear. But because it was always proprietary it has since been lost to time, but its manual is full of all sorts of great example models. If my language can reproduce these, then I'm confident I'll have the right functionality to start.

MB: So… the big question is: where do we want to end up on the functional, procedural spectrum? Should data be immutable? I love the idea of immutable data but the whole point of the model is state change. On the other hand users are going to want to see a history of a stock values... I tried a couple different variations on this with my test models. I played around with linked lists before deciding that was probably more complexity than I needed (truthfully). Then I built a simple model where instead of changing the value, we make a copy of the struct, change that and append it to the end of a list. But I don't like that so much as certain parts of the struct (like the stock's name) stay the same for each copy. Seems wasteful

MB: My next attempt was to make the value of property a list of all previous states of that property. This works pretty well, but as I move from simple models to examples in my DYNAMO reference manual I realize that some models might need values other than the stock might change. For example, it's conceivable that we want some factor to increase or decrease the delay of the flow, right?

MB: I go through a couple of different ways to do that... none of which I like. I mean these are functions, right? We’re talking about something that influences that value of another property. That’s obviously a function. But…Where should those functions live? I like the idea of every propriety in stocks and flow actually being a lambda that either returns a static value if the user defines no function, or the output of said function. But when would that function be called exactly? If it's called every single time the propriety is accessed you could create infinite loops really easily by specifying that two proprieties are dependent on one another. Is that a problem for the compiler to identify and prevent or is that a design flaw? I mean certainly you could do that with most normal programming languages, right?

MB: What do you think Smokey?

SJ: (yowling)

MB: You know… Actually… this is a question I've been pondering for a while: when a given behavior is not allowed what part of language implementation should handle it? When should a problem be a parsing error or a run time problem? Or.... I don't know what ever comes between that.

MB: Let’s google ... "compiler errors -vs- runtime errors” and “language theory" --Oh!

MB: Here's an interesting thought: an exception is not a synonym for error. I never thought about that but I’m looking at a Stackoverflow post that calls them "flow control mechanisms" ... in other words they’re like guide rails meant to keep the program from moving into an undefined state with unpredictable consequences. Errors at runtime it seems are about issues you know are possible but that you can't see coming before the program executes (dividing by zero, for example). Compiler errors are the things you can see coming when parsing the program.

MB: Okay.... um.... well then… back to our initial question. Let’s try “infinite loop recursion compiler error” ....

MB: Huh… It seems that this is runtime error—I guess I should say exception now—specifically something like maximum recursion depth exceeded.

MB: From this point I went down a bit of a rabbit hole looking into how tracking recursion depth is implemented (spoiler alert you increment a counter, obviously) and a bunch of details that just aren't relevant at this stage ... but you know ... when you know close to nothing about a subject, getting off track is inevitable.

MB: Back to functional -vs- procedural... okay. So we’ve got functions. Are these functions pure functions? Absolutely, definitely. Because these are simulations there's no need to connect to a database or make a request to an API. Functions in our model should be side effect free. Particularly if they only exist to define the current state of a given property. This decision at least is easy.

MB: So… they’re pure function but are they first class? Can they be valid parameters? Can a function return a function? Uhhhhhh... I think probably not. Again let's keep things simple.

MB: Last one: strict typing... another strong yes there. If the stock value is an integer there should be nothing in the model that changes it to a string, or even a float. That seems super easy.

MB: I think to start out, if a flow has a precedent defined we will honor that, if not will execute the flows in the order they are declared in the spec. Concurrent flows would be super interesting. It is a real reason why systems fail in real life but for right now it seems like too much to take on. We’ll add that behavior later...

MB: Before wrapping up I'm going to go through a more complicated model from my DYNAMO manual and see if I can represent the same thing with the structures I've laid out here:

MB: Let's see.... Oh here we go. How about an epidemic model-- seems appropriate for our times. This model has three stocks: the susceptible population, the sick population, and the recovered population. On the flow side there is an “infection rate” that moves people from the susceptible population to the sick population and there's a "cure rate" that moves people from the sick population to the recovered populations. Those two rates are influenced by the following factors: the number of susceptible people contacted per infectious person per day influences the rate of infection (makes sense). Also influencing the rate of infection is the fraction of contacts who become sick, and the overall size of the sick population.

MB: The cure rate is influenced by the overall size of the sick population and the duration of the disease.

MB: Over time as I write more and more models I find myself trending towards simplicity. My original draft stocks stored their historical values in a specific "history" parameter before I decided that the value itself could store its own history. My draft flows used to have an increment value that specified how much the flow increased or decreased a given stock. But then I thought, that can be defined in the rate function, can't it? If the rate is constant you can just write a function that returns a constant. Now working on the draft version of this model I find myself staring hard at the target parameter.... Is it necessary to configure the flow to target a specific stock? Can't that also be defined in the rate function?

MB: Wait... no, no. I don't want to do that. There needs to be some way to tell the program where to store the value returned by that function. If we let that happen inside the function itself then we're opening the door to side effects, which we do not want. Okay so targets stay.

MB: Second problem: In this model each flow effects two stocks. The infection rate decreases the stock of susceptible people and increases the stock of sick people by the same amount. The cure rate decreases the stock of sick people and increases the stock of recovered people. How should this be represented?

MB: Perhaps the easiest solution is to create two flows to represent each side... but then how to keep their results in sync? Better to let the interpreter handle this and add a parameter called 'source' to the flow that allows us to specify a stock that should be increased or decreased an inversely proportional amount when the function runs.

MB: In order to represent the factors that influence each flow I have two options. Option 1: we can define global constants. Option 2: either stocks or flows can have additional metadata fields. That should allow for variable factors. In this model, all of the factors are static values, so I'll do them as constants.

MB: The first test is whether the parser can make sense of this model the way it's written-- Great. That worked and the tree looks good.

MB: The second test is whether I can write this model in Go in a way that approximates how the tree will be walked. This implementation will probably get much much simpler when I start writing a compiler, but for right now rewriting the model in a runnable format does help me spot edge cases the evaluator will need to be prepared for.

MB: Anyway... everything looks good and is running smoothly!

MB: Since I have a little extra time I want to go back to the issue of errors. When is something an error and what (if anything) should the language do about it?

MB: It probably will not surprise you to know that there are many different opinions about this. There is no consensus. No authoritative source on the best practices of program language design or postmortems on the mistakes that came before. There are, however, lots and lots of opinion pieces about the issue. You only need to Google "programming language design flaws" to see all the threads on Reddit, Quora and Stack Exchange.

MB: Last night I tried to write a spec in Japanese-- Well not entirely in Japanese, obviously keywords need to be in English, but yeah, could variable names be in another language in my language?

MB: The results were pretty interesting. The spec name was "unikudo" and since that's a foreign loan word in Japanese it's written in a specific script called katakana. But the variable names were the words for "people" "to study" and "knowledge base", are all in Kanji (a pictograph set of characters more borrowed from Chinese). The parser was fine with the katakana, but choked on the kanji. String literals and comments were a-ok though.

MB: So I only have partial unicode support for variable names.

MB: ....Is that a bug though?

MB: Some languages specify that only ASCII can be used for identifiers, some allow a limited set of unicode character. The argument for support tends to settle around the utility of using mathematical symbols as part of the identifier in order to leverage familiar conventions when programming actually mathematical formulas.

MB: The arguments against include things like look alike characters, control characters that reverse the direction, space modifying letters, combining marks ... Unicode characters aren't just a set of letters from foreign languages and some silly pictures. Some characters manipulate the other characters around them. That creates a lot of unpredictable behaviors potentially.

MB: The task of designing program languages seems to be full of "mistakes" that might not actually be mistakes depending on how you look at it. For example, the phrase "null reference" automatically invokes the response "the billion dollar mistake" from language designers. Null earned that reputation after its inventor gave a conference talk titled exactly that: "Null reference the billion dollar mistake." It was intended as a mea culpa. It's true that null pointer exceptions are the most common runtime errors in programming. It's also true that since they could theoretically appear anywhere in a program they are also very difficult to catch. I don't know that anyone has done a survey of this but they do seem to be a key contributing factor to system instability ... and perhaps they have cost various industries billions of dollars.

MB: But after the talk, one audience member pointed out that if you didn't have null references... you would still need to invent them:

Audience Member: The thing is, you have to handle with the actual case, either if you use a technical null pointer or not, you have to check later on. Is it a technical null pointer or is it a pointer to a null class type? Yes, you just delayed the check. And in terms of thinking to fail fast the null pointer allows you definitely to fail fast, which, of course, I mean, a null pointer is a bad thing to happen. But it will— it will happen either, if you have the null pointer or the pointer to the null type

Tony Hoare: I think that’s, that's a very good, very good point.

TH: And I think as a language designer, I would say that language design, the best thing we can really hope for is not to create any new problems. Problems of programming are difficult enough already for the very reason that you suggest there are just so many cases and each case can be tested here or there or elsewhere. And no matter what lovely notations or concepts or checks you put in your language, you can't get away from the fact that there are many more cases that that the program has to think of and deal with all those cases. It doesn't really make programming easy, it just removes one of the difficulties.

MB: And yes, if you watch the full video you'll see someone jump up to talk about Haskell right away. So don't worry Haskell fans. It was covered.

MB: Another famous "mistake" in program language design is the ambiguous nature of grammar in C++. It makes C++ almost impossibly complex to parse and yet C++ is still one of the most popular languages. A large part of that is probably because the users of C++ are not likely to ever need to write a parsers for their own programs, they just used the compiler that's already solved the issue.

MB: Still there are others that are open for debate. Is the plus sign handling both addition and concatenation a mistake? If you forget a break statement at the end of the case block of your switch statement in any C based language and the program will execute the case below. Is that a design flaw?

MB: While working on my language someone pointed out to me that none of the major programming languages were written by academics studying program language theory. Some language inventors worked in research labs and most have advanced degrees in computer science. But the languages that actually get traction tend to be invented by professionals who designed them based on their own pragmatic needs and purposes. So the question of when is a mistake a design error to be corrected or a user error to be documented but ultimately left alone is tied to utility. What value is lost by allowing a program to break? What does the user gain in being able to do unexpected things? SHOULD my parser recognize identifiers in unicode?

MB: Another point to consider is how many of the design flaws in programming languages have more to do with the environment changing around the language rather than the language designer making a mistake. Javascript and PHP were not invented for the internet of today. Things can become flaws when the usage patterns around them change.

MB: Ultimately we can't do anything about that. We can't predict the future. We can only figure out the use cases for today. And the only way I know how to figure out user utility is by talking to some actual users...

From Parse Tree to Evaluator (featuring Sarah Withee)

Marianne — Wed, 09 Dec 2020 04:16:11 +0000

Summary

A parser generator like ANTLR won't handle evaluating programs written in your new language. You need to write the code for that yourself. Marianne explains how to build an AST from a parse tree, create an evaluation loop, and how esolangs (esoteric programming languages) make for great learning tools.

Bonus Content

Become a patron to support this project.

Book Club: Thinking in Systems

If you're interested in learning more about stock/flow system models or have just had Thinking in Systems by Donella H. Meadows on your reading list, I'm giving people a free one month pass to the MWaPL private community for patrons in order to read it with us. Request a free pass here

Transcript

MB: When I first started releasing episodes of this series a few people asked me to put them up on Youtube as well as traditional podcasting channels. This is going to be the episode where that comes in handy. Today I’m going to talk you through how you take the output of a parser generator and build an evaluator loop on top of it that can run programs. If you find yourself thinking “I really can’t visualize what she’s talking about”, I encourage you to look up this episode on Youtube because the Youtube version includes screen caps of code that might make it easier to understand.

MB: Funny enough in my first draft of this series this episode did not exist. That’s the challenge of learning things— once you understand them, they begin to feel obvious and trivial and you forget that they have to be explained to other people.

MB: Right. So...

MB: If you decided to write your own parser then the question of how to connect the parser output to an evaluator loop is simple, but if you’re like me and you wanted to leverage the mature tools that exist to do some of this stuff for you it is not immediately obvious what you should do after you’ve fine tuned your grammar and generated your parser. A parser is NOT a programming language.

MB: I’ve been using ANTLR to generate my parser and lexer so some comments will be specific to that, but the general concepts will be applicable to other tools so you should be able to follow along if you’ve chosen something else.

MB: In the language I’m building I don’t want global functions. Therefore when we think of a grammar as breaking a file into smaller and smaller chunks of valid code there are only three types of code that can be in a program: declarations, assertions and for statements. The for statements I’m referring to in this programming language are a bit different than you’re expecting. Because stock-flow models are themselves designed to run in a bounded loop. The for statements in my language are not for loops, the are configuration settings for the model’s internal loop.

MB: But I digress. Assertions aren’t really important at this stage of the language development so that leaves just declarations. The first level of our grammar is the spec file, the second level is a set of declarations, the third level are all the possible declarations: constants, stocks, and flows.

MB: Stocks and flows have proprieties and methods, some of which are required default. By this point you should begin to see how this forms a tree: at the root we have a spec node, under that a declaration mode, under that the specific type of variable we’re declaring … maybe a stock node, with that node we have a series of property nodes. Under a property node maybe a function definition… under that……

MB: This is what the parser will create. It will use the grammar to define how to break source code up into a set of nodes arranged into a tree, then it will walk that tree for you.

MB: But walking the tree isn’t executing the program, that’s the gap we need to write code in order to fill in.

MB: In ANTLR part of our generated code will include something to walk the parse tree (either a listener or a visitor depending on how you configure ANTLR). A listener will walk the entire tree from top to bottom and then back up, executing your custom instructions as it goes. A visitor will only move forward if you tell it to advance to the next node, which can be useful if you don’t need to consider the full program. For example, part of the REPL I built to do user testing outputs a visualization of the model, but that visualization only cares about which flows are connected to which stocks and how, the rest of the code isn’t relevant. So that’s a situation where I used a visitor instead of a listener.

MB: Both visitors and listeners will generate a set of hooks for each node. So what you do is extend the default class that ANTLR has generated (be it visitor class or listener class) and overwrite those hooks with custom code that extracts the data from the node and assembles something executable out of it.

MB: In a prototype language what this means is that I have a hash map where I store defined variables. When we walk the parse tree and encounter a declaration node, we pull the identifier out of that node (often a child node of the declaration) and turn it into a key in our hash map, then we pull the assigned value in the declaration node (again often child node of the declaration node) and store it as the corresponding value.

MB: This is super easy when the values are static— strings, numbers, etc. But what do we store when we declare a function?

MB: Well… We store a tree.

MB: I suppose you could store a copy of all the relevant child nodes from the parse tree, but I actually found it easier to create a simple AST. That’s Abstract Syntax Tree if you’re unfamiliar. ANTLR’s parse tree has a lot of information in it, after all. And parse trees tend to contain nodes that accurately represent the syntax of the grammar, but are not important to the execution of the code.

MB: Building your own AST is not super difficult. Essentially every node needs to store some information about its type and then a value. The node value will either be a child node, a set of child nodes, or a static value like a string or a number.

MB: Since I wrote the prototype in Javascript I could get by with having one node class the type being stored as a string in a property. When I start building the real language in Go, each type of node will need to be defined as its own type in Go, because Go will enforce strict assignment of the node value property which means it can’t be a single child node or a slice of nodes or an int or a string…. we have to define exactly what it going to be up front, so we have to define a different node type for each node we want to use.

MB: I mentioned before that when we extend ANTLR’s generated visitor/listener class we get hooks for each node of the parse tree. We will have code that triggers when we enter a node (its name is enter followed by the node name as it is defined in the grammar, depending on what language ANTLR is compiling to it might be enter plus node name plus the word context, the best way to know for sure is to open up the auto generated visitor or listener file and check) and then there’s code that triggers when we’re exiting the node as the walk is moving back up the tree (that has the same naming convention as enter hooks just with the word exit instead). Most of the time you want to use the exit hooks. We’ll talk about why in a second.

MB: We build the AST by wrapping data from the parse tree node at the very end of a branch in the right AST node type and pushing it onto a stack (which in most languages will either be a list or an array). That’s why the exit hooks or so important, because we want to start from the bottom (where the data is) and pass AST nodes up. That way when we get to the part of the parse tree where we define our function and assign it a name, the AST is sitting on the top of the stack, fully formed, waiting for us.

MB: As we move up from the bottom node, whenever a higher node has valuable information, we need to sort of add to our tree, we pop off the top of the stack, wrap that value in another node capturing the new information and push the larger tree back onto the stack.

MB: So for example: let’s say I have the expression x + y. We have a node representing x, a node representing y, and we want to wrap them in a parent node called addition. Using this structure allows us to create complex algorithms with the same code we do for simple ones. A+b+c is just an addition node where one child node is c and one child node is another addition node with child nodes a and b.

MB: Building ASTs is useful because most functions will make use of values passed to them at runtime, so you can’t execute them while walking the parse tree because they may not have been defined yet.

MB: When we finish walking the parse tree what we have is a hash map populated by all the named variables and the values assigned to them and all the named functions and the trees that represent the steps they execute.

MB: Since stock flow models operate in loops, walking the tree gets everything defined and assembled then the process of executing the model loop pushes those new trees into the eval loop.

MB: The eval loop is a function wrapping a giant switch statement. The value being tested in the switch statement is the type of node being passed to the eval loop and each case typically calls the eval function recursively passing in the node’s child. It the node has multiple children the case block will call eval on them all one by one. Sometimes in a for loop or sometimes in a different construct depending on what the node actually does.

MB: So our x+y example from before would operate like this. The switch statement would evaluate to node type addition add return eval(leftNode) + eval(rightNode). When the eval loop executes on the leftNode, the leftNode type is a variable, the case block probably says something like look for a variable by that name in the hash map and return that value. It this way we work down the tree until the eval loop encounters a value it can actually return and then the recursion completes by passing those values by up.

MB: The best way to understand how this works is just by doing it a bunch of times. Every time I work on an implementation I get a little bit better at it.

MB: But if you’re thinking to yourself that building an interpreter or a compiler over and over again sounds like a lot of work— you’re right and I have a suggestion!

MB: To help with my suggestion this week I asked my friend Sarah to come on the show. Sarah is another Strange Looper who I also know through the Pittsburgh based hackerspace and community group Code & Supply. Hey Sarah what are you working on now?

SW: Currently working on a side project called Code Thesaurus, which is a polyglot developer reference tool, so the idea is if you know something in one language and you're wanting to know how to do the same thing in a different language, you can look it up in the tool and kind of compare them side by side without having to, like, read entire sets of documentation. You can just kind of see a quick glance at a chart and kind of know the difference between the two.

MB: So if you hear a little background noise that’s because Sarah’s completely adorable cat Theodosius keeps swatting at her microphone. Anyway, back to my suggestion: Esolangs. If you want practice tying everything together, work on a few esolangs first.

MB: Sarah, do you know what esolangs are?

SW: I believe they're esoteric languages

MB: Yes, they are. They're this fabulous world of, like, really weird, strange, completely compilable valid programming languages. Right?

SW: They are basically like, hey, I don't think we should ever do this, but let's do it anyway.

MB: Yeah.

MB: Like, wouldn't it be great if we lived in a world where we programmed only in white space.

SW: Something you would never really want to do, or only in symbols or only in colors?

MB: Yes, the actually the only in colors ones are the ones that I like the best. So is it P*iet or Pie*t? I never quite clear how it's suppose to be…

SW: I call it Piet, but yeah, I don't know…

MB: Okay. We’ll go with Piet. It’s sad because it's someone's actual name and so… I should have done the research.

SW: I think it’s an artist name.

MB: Yeah it is. But like I was looking at some of the programs that people write with the this programming language, which is essentially just about interpreting colors and like pixels. They're gorgeous! Like people have done like almost like meme style portraits in this language and they've done beautiful rainbow mosaics in this programming language. And like I wouldn't say that any of those programs are useful. Right? Like mostly I think what gets written in esoteric languages are like hello worlds of various types that either print hello world or like print the name of language is super popular or they do calculators like this is how you program a calculator in this particular language, what's not clear to me is like where the line between an esoteric language and like a domain specific language is like how useful do you have to be before you’re a domain specific language?

SW: I don't know if I know where that solid boundary is either, but I would say, you know, typically you want a programming language to be readable and readable and like easy to convey your thoughts in the form of code and esoteric languages are almost never any of that.

MB: That's true.

MB: Well, I think like we do like as programmers care about the look of our code, right? But esoteric languages are almost inevitably like this bizarro world where the the actual look of the source code is more important than what the source code does or how efficient it is it doing it. Right?

SW: Yeah. You know, they're usually proof of concepts like can we actually use LOLCat as a way to write a programming language?

MB: Oh….. I love LOLCat so much. Can you talk a little bit about like, what is LOLCat?

SW: So LOLCat is like the memes of the cats, of, like, I can haz cheeseburger nonsense and like the embodiment of what if your cat were to actually talk to you and has bad spelling and grammar. But it's like what if you implemented that as a programming language like O HAI. O Space H-A-I would be like the introduction to your program and you know, like I can haz variable name would be like to set up a new variable and I don't remember too much past that, but you know, it's like you can have these things in their typical statements and they're not super easy to parse. Kind of like if you took Shakespeare and decided to write it in LOLCat like it's doable. It's not readable. And you may have to sit there scratching your head for a little bit, but, you know, you can convey the same thoughts. And so, like, LOLCat is one of those. It's just silly, you know, like out of like completely out of the box, like Piet or Whitespace or some of the other ones.

MB: I really love how LOLcode ends blocks in KTHXBYE. I want to do that in normal programming languages. It's just way more satisfying to write KTHXBYE instead of like END, right?

SW: Yeah, sure. Well python has some of that really readable text in some ways and Cobol even kind of have some of that.

MB: Yeah. But it's interesting that you bring up Shakespeare because did you know that there's also an esoteric language called Shakespeare?

SW: I believe I've heard of it. I don't know that I've really looked into it that much.

MB: So this is what I find really interesting about esoteric languages is kind of weird, like bizarro world form of like prioritization in code.

Shakespeare, the programming language is a programming language where your commands are meant to sound like lines from a Shakespeare play and your entire source code it has to be architected in a way that mirrors like stage directions. But in order to accomplish this, they do a couple of weird things. So they essentially sort— it's like a very keyword heavy language. And they sort nouns and adjectives into categories of like positive numbers and negative numbers. And so every noun is like a positive number of one or a negative number of one. And then you use the adjectives to sort of build upon them. So like say, look, I like I will add an adjective to one value and that gives me a two value. And if I add three adjectives to one value, I now have four and so on and so forth.

MB: And so it's like ridiculously complicated. But one of the critiques I read about Shakespeare, which I thought was interesting, is that it's actually… that kind of control flow is actually very similar to Assembly, but— Shakespeare itself, like all the implementations of it, are essentially kind of more transpiler than they are interpreter and compiler, so the main implementation of Shakespeare will parse your Shakespeare and then write a C program based on like what it's found in your program. And there's one I think that doesn't it in Python. And then what you're running is really a C, C or Python program. And since Python ultimately compiles to C, I guess ultimately just ends up being a C program. But what's interesting to me about that is that if your actual structure of your esoteric language is kind of mirroring the pattern of Assembly, like why are you translating it to a high level language that gets—that ultimately gets compiled down to assembly? Right? Like we're kind of going around in a circle in order to, like, get this joke of like, hey, we've got a programming language that looks like Shakespeare.

SW: But I think you also underestimate, not only the love of nerds to do weird things, but the love of nerds to go. I bet we can't do this. Watch me.

MB: I do historically underestimate the love of nerds to do weird things. It's true.

SW: Because I believe also you're writing a programming language, which is also kind of this like, hey, nerd, can I actually do this?

MB: Yeah, I know that's totally fair. It is totally 80 percent. “Hey, can I do this thing?” nerd-ness and like 20 percent this thing might actually have a useful function in problems that I face and other problems that other people face. It's true.

SW: And you've heard of like Ook? The language Ook, right?

MB: No. I haven’t.

SW: It’s supposed to be based on the sounds of monkeys. Oh, like Ook would be O-O-K. So it's either ook period period would be like maybe the start of a program like ook period. Question mark would be how you know like create a variable and question mark period would be something like, you know, add together and there's a whole list of the different ooks and the combinations of them that perform different actions.

MB: Oh my God. How do you…

SW: It's supposedly Turning complete if I remember correctly.

MB: I've pulled this up on Esolangs.org, which is like literally is the ultimate guide for every bizarre programming language that exists. And it's just like looking at the Hello World Program. It's just like it's ook? Ook, ook, ook. OoK, ook. OoK, ook. OoK, ook.

MB” This just goes something like that forever and ever and ever and ever. Ook is a David Morgan-Mar—so danger mouse— creation and like this seems to be like, it seems that the David Morgan-Mar really does very little except like draw cartoons and then write esoteric programming languages. He, he is the creator of Piet that we talked about before. He's the creator Chef, which is similar to Shakespeare in the sense that you're trying to get it to look like something else, but you're trying to get it to look like recipes instead of Shakespeare. And like there are at least eight different esoteric languages attributed to him. One of them I’m pulling up now is called Zombie. It's a zombie oriented machine-being interface engine designed for necromancers and pure evil ones. Programs run in a multithreaded environment where they're every kind of entity zombie, vampire, ghost, demon, dijinn, and they all act in a slightly different way. A program is a list of entity declarations stating the action that each entity must perform.

MB: Oh, it's a declarative language! It's sort of like the trolly version of Prolog.

SW: (laughs) I like that description.

MB: I now kind of want to write like a model validator in zombie and see how that would work.

SW: And you’ve heard of like the emoji language, right?

MB: Yeah.

SW: And every commands are just emoji symbols.

MB: Yeah, that's true. Emoji language like one and some of the ones I was looking at today is there’s a language called Don't, which is described as it only has three commands. Command H prints Hello World. It's the hard part is done for you, basically. Uhh the question mark teleports the user's device to a landfill in Dubai … which seems useful depending on what computer use.

SW: I can dig that.

MB: And then the last is G[] which deletes don’t from existence. And then the explanation of don't is unfortunately someone ran the G command and one of their programs while testing an interpreter, causing the language to be removed from everyone except the creators of memory. It was rendered impossible to implement….. So there you go.

SW: This language doesn't sound Turning complete.

MB: No, I don't think so. I don't I don't think so. There's also Retina, which is based entirely on regex. So like no syntactic sugar, just pure regex in case you wanted to put all the bad parts of programming into its own language. There you go.

SW: I’m constantly amazed at I feel like every time I look at the site, they've added like a whole ton more languages to it. Like I'm always just baffled at the absurd lengths people go to. I mean, like some of them are kind of fun and interesting, you know, like some of them are made as jokes. Some of them are made to be funny, but some are made to like absolutely to screw with people's heads.

MB: But I think in general, esolangs end up being really useful learning tools, because their very design usually relies on an extremely limited grammar and extremely limited vocabulary set. So you don’t have to think about, like, how do I implement like all sorts of complex data structures in order to like design a parser, a lexer and ultimately an evaluation loop, you can kind of just start off with a really simple scope and kind of like work those muscles over and over and over and over again as you as you need.

Writing a BNF Grammar (featuring Prof Jeff Heinz)

Marianne — Wed, 02 Dec 2020 04:54:15 +0000

Summary

Writing a programming language starts with its grammar. But what is a grammar in the context of computation? And how does one go about writing one? This week Marianne talks with computational linguist Jeff Heinz about Alan Turing, Noam Chomsky and what context-free grammar actually means.

Bonus Context

Become a patron to support this project.

Transcript

MB: This is going to be a great week. Because this is the week I actually start implementing things. Are you ready? Okay, let’s get started!

MB: What you're doing when you write a programming language is actually writing a series of applications that take string input and translate it into something the machine can execute.

MB: The building blocks of programming language implementation are: parsers, lexers, and evaluators. Lexers take your code and break it up into parts. Parsers assemble those parts into trees that suggest semantic meaning. Evaluators walk the tree, interpret the meaning of each leaf and execute the appropriate behavior on the machine.

MB: I wouldn't necessarily say that this stuff is easy to understand, but there are enough explanations out there (some very academic, some more plain language, some with examples, some heavy on history) that after I read two or three of them I felt pretty confident about it.

MB: But for me at least, the hardest part of learning something is figuring out how to learn it in the first place.

MB: The thing is... just about every resource I studied on parsers said the same thing: this isn't how you would do things if you wanted to do this for real. If you were going to do it for real you would use a generator.

MB: When I raised my hand and told the internet "hello I'm going to do it for real, what do I need to know to use these generators?" dead silence came back.

MB: There are only two types of people who write the code for parsers from scratch: absolutely beginners and absolute experts. The beginners write parsers "by hand" so that they can learn HOW they do what they do. The experts write them so that they can optimize them within an inch of their lives.

MB: Everyone else, as it turns out, writes a grammar that a generator uses to write a full lexer-parser for them.

MB: There are huge advantages to generators. You get to leverage the experience of the whole language design community and control for edge cases and errors that would probably never even occur to you. You also make it easier for other people to implement your language, as most generators accept the same formats for grammar. And lastly, you have less code you need to write when you use a generator.

MB: Since I wanted to implement my language in Go, selecting a generator was really just about which ones generate parsers in Go or not. Skimming the Wikipedia chart, I picked one out and I started reading the documentation. Accepted grammars in EBNF, cool, well what does that look like?

MB: ...you know... Confronting what feels like a tidal wave of information is becoming an all too familiar feeling on this project. All the tutorials I could find on writing BNF grammars seemed to assume you understood the mechanics of grammars in the first place. I'm basically looking for Strunk and White's Elements of Style in the Microsoft Word Help Center ... that's what it feels like.

MB: Something that kept getting referenced over and over and over again without much of any context to hint at why it was relevant was Chomsky's Hierarchy, Chomsky "context-free grammar" also "Chomsky normal form" ... but coming from a position of complete ignorance, it is hard to understand how these concepts map back to the work of parsers.

MB: So I reached out to a friend of mine who is a linguist and happened to study under Chomsky. Did she know anyone who understood both the world of the programming and the world of linguistics?

MB: Oh... she said, Yes! You should talk to Jeff Heinz out at Stony Brook.

MB: .... I have to confess that I'm vulnerable to a certain degree of magical thinking. I did my bachelor's degree at Stony Brook, so this felt right somehow. Then when I looked Professor Heinz up I saw he had given a joint talk on grammar -vs- statistical approachs to natural language processing which they had promoted it by producing a parodying a heavy weight boxing match.

MB: Yeees... I think this is the right person to talk to.

JH: So right now, we're in the age of big data and a lot of the hype around artificial intelligence and machine learning is that you can provide these sort of general learning machines with lots of data and it's going to learn what it is that it's supposed to do. And I don't think that's how children learn language at all. I think children learn language from actually small amounts of data. And I think that the big data, I mean, even in our own world of big data, is good for languages like English, French, Chinese. But, you know, there's thousands of languages and there isn't a lot of data for most of those languages.

JH: But children will learn those languages of the raised in those communities, again effortlessly. So my own feeling is that I want the computing, the learning algorithms, the machine learning algorithms and the AI algorithms to learn more like people do. And what that means is that they're going to learn from small data. And the way that they're going to do that, I believe, and what I'm working on now is currently the these machine learning algorithms, they need big data because they're searching for the needle in a huge haystack. And that's actually... so they frame the problem wrong. In the case of natural language, we're not searching a huge haystack. In fact, it's a very small little pile of of straw and the needles right there.

JH: And so the thing is, what's that small pile of straw? What's that? How do we characterize natural language in the right kind of way? So the search problem is actually very easy.

MB: Something I had been unaware of until I started digging into generators for parsers is how useful both parsers and grammars are for other challenges outside of implementing programming languages. I feel like I've been struggling to hang pictures around my home and one day someone knocks on my door and introduces me to the hammer. My career is filled with all these challenges that it turns out I just should have written a parser for.

*MB: Like data transformation, should have wrote a parser for that. Log alerting? Parser. Allowing rich search querying? Parser again.

MB: But when you tell me to write a grammar for my programming language ... I don't even know where to start. Obviously a grammar is a list of rules. But what kind of rules even go in a BNF grammar and what sort of things are handled by error handling on the evaluator?

MB: How would you actually define what a grammar is, because most people associate the word grammar with what they learn in school, which is a variety, which includes grammar, but also things like spelling and syntax and all sorts of different concepts. And most software engineers, when they think about software, what they're thinking about is not grammar. They're thinking about syntax. Right. So, like, how would you explain what a grammar what a formal grammar actually is?

JH: Yeah, so...

JH: So a formal grammar, I would explain, is just any kind of device that's able to take a sequence and tell you whether it's valid or not. And that's that's it. And so in some sense, it's going to identify some subset of all logically possible sequences, the ones that are valid. Now, you can have you know, that could be a very large set. It could be there could be infinitely many strings in that set. Sort of like you can think of the set of all even numbers. You can think of all the strings that begin with an A or the word the or whatever you want. Those are... And you can write formal grammars that would recognize those strings. And so that is in one sense what a formal grammar is. And it can be... it can take many forms. I mean, so people have studied formal grammars from logical perspectives. They've studied them from sort of machine type perspectives, from algebraic perspective. So you can study these formal grammars from many perspectives. Having said that, I would say that a grammar in the sense that people will typically use it like both in software engineering and I would define a little bit differently than a formal grammar. So the formal grammar is just focused on, say, the set of strings or sort of structures more generally. Doesn’t have to be strings. You could be talking about tree structures or graph structures. So any kind of object you're interested in, the formal grammar is essentially a classifier.

JH: It just say these are these are going to be OK and they're not going to be OK. Now, why would you care about that?

JH: Well, as you said, in software engineering and natural language ideas, you're going to try to interpret... you want to interpret those those structures that are admissible as valid structures. And so the question is... So that's the other part of grammar that I would say is important, is that not only is it just a set of structures or something like that, it's actually... More and more abstract. It’s a way of trying to go from the structure that you see to something else, to some kind of meaning, some kind of semantics.

JH: And so this is also why we study, because we often think of the syntax, in a sense is part of the grammar that gets interpreted in two ways. So one way is sort of the linear string that, you know, that you would write out, which would get passed into that syntactic structure. And the other one is going to be the meaning of that. So that's going to be the the instructions to the computer, how to fire up the circuits in certain ways or the meaning that we're expressing when we're talking to each other. So the grammar is is is sort of fundamentally this connection between. The linear string that's being expressed and the meaning that's being expressed by that string, it's that connection.

MB: So we need to think about it in terms of the structure of our strings, in this case code-- As it happens, the best resources I found for how to think through this were the reference manuals for the generators themselves. This caught me a little by surprise because ... you know, I don't expect to read about the vanishing horizon in the manual for Adobe InDesign, right? Reference manuals assume you know what the tool is for and just need to learn how to user the tool. But I guess I'm not the only one who has no idea where to start with grammars.

MB: My favorite resource so far has been The Definitive Antlr 4 Reference by Antlr creator Terence Parr. The book includes common patterns in grammar and step-by-step example grammars for real world languages.

MB: So... Here's how Parr recommends starting: go from the largest complete unit of the string down. So in other words, the first rule should define what a file is ... what is a file made up of? And the answer to that could be lines if you're parsing something like CSV, or it could be multi-line objects for JSON. Let's say it's an object... what is the object made up of? Key-Value pairs, right? What are the keys made up of? What makes a key valid versus an invalid key? Strings with double quotation marks if we’re talking about JSON. What about the values? What makes a valid value versus an invalid value?

MB: ...And so on. Each description of a new level is a new set of rules to implement.

MB: All this is well and good, but when does the context-free part come in?

MB: So in the world of language design and language development, we hear about Chomsky all the time, particularly around Chomsky's hierarchy, like what is Chomsky's hierarchy in linguistics? And like, does it connect to an underlying philosophy in any way?

JH: Yeah, yeah, it does so so Chomsky's hierarchy is... so Noam Chomsky is a famous linguist and intellectual, arguably one of the most important figures of the 20th century, at one point, one of the most cited people in the world of all time. And he's someone can be somewhat controversial, I guess, in both in linguistics and in his political writings. But there's no question his impact has been kind of enormous. Having said that, I also will say that... you know I saw him give a talk several years ago at the University of Maryland, actually, and he just began by pointing out how, you know, the way that most people view language in the broader context of cognition. Nothing's changed in 50 or 60 years. They all view it as just something that is just like any other aspect of cognition. And there's there's nothing... You know, there's nothing about it in particular, and you see that in a lot of work outside of linguistics proper... in cognitive science and so on, people are trying to tackle the language learning problem just like they would tackle any other problem. So they're not necessarily trying to focus on features of language per se. They're just focus on general features of cognition. So I was quite taken aback, but I'm thinking here's a guy who's done more than anybody else to sort of challenge that view. And he's saying, actually, there's really no difference between now and 60 years ago when you look at the broader scientific field. I thought that was quite interesting.

JH: Well anyway, so what is the Chomsky hierarchy? So the Chomsky hierarchy is actually a sort of a refined view of the notion of computability more generally. So, you know, one of the big advances in the 20th century was this notion of what is computation. And there are several figures who contribute to that. The most famous one now is Alan Turing, but he's not the only one. There was Alonzo Church.

MB: Right.

JH: There was Kurt Gödel. There was all these guys in the 20s and 30s really made these. You know, incredible... I don't know how to describe it, but they pointed out in a way where they showed you what is computable, and so they show that there are certain problems that, you know, no computer can compute. And by computer, they don't just mean the hunk of metal and plastic on your desk or your phone. They mean anything that computes, which is sort of, you know. Including people, people are in the information processing systems, they are, in a sense, computers just they're made of a different type of material than than the phone in your pocket. So. So so there's sort of an outer limit of what can be computed.

JH: And so, for example, what Alan Turing showed was that most real numbers ... actually real numbers— real number is just like pi, 3.41 goes on and on and on. Most of these numbers cannot be computed. And by that, what he means is that like for pi, you can give me a number like five and I can tell you the fifth digit of pi. And if you do the number like 10 million. I can follow some kind of computation and eventually I can give you the 10 million digit of pi and they're programs that are running this stuff all the time. But most real numbers aren't like that. Most real numbers you can give me— There's no algorithm for which you can give me a number N and I can give you the nth digit of that real number.

MB: Yeah.

JH: OK, and so that's quite interesting. So there's a question of what— So that's the limit of computability. So what's the Chomsky hierarchy if I said it. So now, you know, I’m— I don't know. I think probably belaboring this point too much.

JH: You're I'm thinking too long to get to the point. But the when you refine the hierarchy, you find that you're asking, OK, suppose I have... So that's if I have all the resources and time in the world. Suppose I limit my resources in some way. Now what what am I able to compute? And so that's how you get these different. And if we do this in string space instead of in number space, what can we do? OK, so I mentioned before how formal grammar can distinguish between this set of strings as valid or not, these string are not valid. So that's sort of a computational problem, which is sort of the same. If you want to recognize a number or identify a number by knowing what the amplitude is, you want to be able to identify a set of strings by saying, is that string in the set or not? Okay?

MB: So the hierarchy isn't so much about the complexity of the grammar, so much it is about the computational abilities and the level of specification of the grammar.

MB: Is that a good way of summing it up?

JH: Well, it is about complexity of the grammar, but it's also it’s... What the Chomsky hierarchy does is it identifies different types of computational resources that you need to solve different types of... I would use the word membership problem to describe this, this problem of is this string in the set or not on the set?

MB: Got it. Got it.

JH: So if I if we have the term membership problem, then I would say to the Chomsky hierarchy classifies membership problems. Over strings

MB: OK.

JH: Over sets of strings. The reason why I hearken back to the dawn of computer science and this whole thing in this long story that I'm telling is because it wasn't just about linguistics. I mean, the context free grammars, which is sort of the part of the context of the Chomsky hierarchy that Chomsky introduced that... that became the basis for programming languages and compilers and all that kind of stuff. So when you when you're going to write your own programming language, you're going to have to learn something about context free grammars.

MB: Right. Right.

JH: And there's no way around that because that's what's used. I mean, all of these programming languages are essentially content free. Yeah.

JH: And that's not the only type of I mean... that's a very important region in the Chomsky hierarchy. And we can ask the question, are all natural language patterns, you know, in a sense context free? And the answer to that question appears to be no. When you look at certain kinds of syntactic patterns, you have to go outside of that. You don't have to go all the way to the Turing complete computer.

JH: There's an area called context sensitive.

MB: Right.

JH: And that seems to be where we find natural language patterns

JH: In my own work in morphology, phonology, context-free actually seems to be more than sufficient. And you can go much smaller than that. The last thing I would say about the Chomsky hierarchy is that many people, when they when they study it, you know, it's in all the computer science undergrad courses. You have to take a course in automata theory and you study the Chomsky hierarchy and complexity and so on. And people and they all know that this was work that was done 50, 60 years ago. So many people think that was a chapter that was opened and closed and that's it. But that's not the case. The fact is that in the past 60 years, there are new chapters constantly being written with those same methods. And we have much better knowledge now about, I mean, the Chomsky hierarchy is just the most famous of many, many types of hierarchies, many, many types of ways we can study sequences, structures, objects, transformations from sequences to other sequences. So machine translation, you know, you want to you want to translate the sentence in French to a sentence in Swahili. You know, those those are all things that formal language theory studies. And there's many more hierarchies beyond just the Chomsky hierarchy that are relevant to these problems. And so there's... it's a very... it's an alive, living area.

MB: Uh, this is so interesting.

MB: So, like, what's particularly compelling to me is when I was first exposed to the Chomsky hierarchy in the context of writing, programming languages, my first immediate assumption is this is a metaphor, right? That this is something that we have misappropriated from another field of study to provide a little bit of visualization behind what these like really kind of abstract grammars mean. And it doesn't actually connect to anything specific to computation. And what I'm hearing is, no, no, no, that's completely wrong, that it actually is all about computation and the level of computation needed at various parts of the hierarchy, which is not what I was expecting to hear, and that is super, super interesting.

MB: After my conversation with Professor Heinz I went back to the things I had read about Chomsky's Hierarchy. But this time I reread them with computation on my mind.

MB: And just like that, it clicked. The lowest level of grammar in Chomsky's Hierarchy is what's called a "regular grammar" .... as in a regular expression. When a regular expression matches a pattern in a string, all it knows, all it needs to know to determine that match is what is directly in front of it at the time. And from this type of parsing we can deduce a certain level of meaning. But you couldn't use regular expressions to parse a programming language, because the same characters can have different meanings in programming languages depending on how they are used. Think about the equal sign: by itself it could be assignment, with another equal sign it means something different, with an exclamation mark... still another meaning. So in order to parse a programming language, you need a little more computation... you need to factor in whatever came immediately before. Those are context-free grammars.

MB: Above context-free are context sensitive grammars. Most spoken languages are context-sensitive. In English it's not enough to have the word directly before the word your trying to figure out the meaning of, we often need the whole sentence up to that point ... still more computation. And so on and so forth.

MB: OK ... I feel ready to start writing this grammar!

MB: I really like the look of specs written in Alloy, so I'm gravitating towards using that as my inspiration. An Alloy file is made up of hash map looking structures called signatures, blocks of logic code, and short one line statements that define what the model should check and at what level of complexity. You can even import other models, although this doesn't actually work they way I want it to in Alloy.

MB: Our spec files will start with a declaration statement giving the model a name. That's one line.... let's use the keyword 'spec' followed by a valid identifier. Identifiers are alphanumeric but the first character must be a letter (in order to keep them from being confused with actual numbers by the parser)

MB: After the declaration statement we'll have an import block. Let's do that the same way Go does it: keyword "import" followed by a left parentheses, followed by a set of strings with import paths, followed by a right parentheses. .... Yeah, I like the way that looks.

MB: At this point I compiled the grammar and started experimenting with how that was looking in token form. Antlr 4 let's you determine what things the parser handles and what things the lexer handles by modifying the case of the nonterminal symbols .... basically what that means is that each line of the grammar looks like a variable assignment, the left hand side (the nonterminal symbols) are like variable names and the right hand side are the rule definitions. And yes, there can be multiple rules joined by a '|' as an OR, and they can also be recursive. But for a simple example the rule to parse 2+2 might read something like INT "+" INT.

MB: In Antlr 4 if the nonterminal symbol begins with a lowercase letter then the rule belongs to the parser, if it begins with a capital letter it belongs to the lexer. The distinction is what gets treated as a token (rules belonging to the lexer) and what gets treated as a string to potentially be broken up into more branches and nodes on the tree (rules belonging to the parser).

MB: So far this grammar is just for a tiny header that names the spec and imports other specs. After that are our blocks of code and that's more complicated. If we're using Alloy specs as an inspiration than we will have hashmap like structures that defines the elements of our system. Therefore the next rule is that there will be one or more entities. Entities are defined by the keyword "def", followed by an identifier, followed by an equal sign, followed by a left bracket, followed by a properties list, followed by a right bracket.

MB: What do the properties look like? Well... They start with an identifier obviously (the key), followed by a ':', followed by a value. For the time being the values will be either integers or strings. We don't want to get too complicated before recompiling and looking for errors.

MB: The final grammar will need to be more robust than this, but this is the way I worked through it: starting simple, compiling the parser and lexer, inputting a mock spec and fixing bugs before adding more complexity.

MB: It is incredibly satisfying when it gives you the output you were expecting.

Certainty is a Programming Bug (featuring Hillel Wayne)

Marianne — Wed, 25 Nov 2020 04:24:56 +0000

Summary

What kind of programming language is Marianne trying to write? Before we go any deeper into the guts of language design, Marianne and friend Hillel Wayne debate the shortcomings of various approaches to specifying and modeling program behavior. From first order logic verification to system visualizations, nothing Marianne has used before has quite fit the bill. She's beginning to get philosophical about the nature of abstraction and wants to rebel from the goal of certainty.

Bonus Context

Become a patron to support this project.

Transcript

MB: The first thing every guest has asked at the beginning of every interview is: What exactly are you trying to do?

MB: So I figure before we get into the details of how to do it, I should spend some time answering that question in detail. Talking with me today is my friend Hillel Wayne. I met Hillel a few years ago at one my all time favorite tech conferences, Strange Loop. Hillel is… well, I'll him introduce himself:

HW: My name is Shlomo Hillel Wayne, but I go by Hillel Wayne, almost exclusively, I am an ex-physics major, ex-web dev, now I teach formal methods--the science of writing software blueprints in a way that can be verified directly as opposed to after you build the system--full time. I also do a lot of writing on tech, tech culture, tech history and sort of the journalism and sort of culture of tech. So I sort of at this point, my job is mostly a mix of teacher, historian, journalist and writer.

MB: The science of writing software blueprints. I like the way he puts that. But there's been something that's been bugging me about formal specification for a while now that fuels this project.

MB: How to keep people from misusing them?

MB: People gravitate towards models, much like statistics, because they feel like it reflects objective truth. If you're looking to build models because you want help reasoning about the world, your system, and decisions we face with both, then just about any modeling language will do. Python will do.

MB: But that's not what a lot of people look for when they model things. They don't want an abstraction, they want a guarantee. For that reason, formal specification stays on the fringes of software engineering. Unit tests feel like they offer a guarantee, models of software systems - on the other hand--can run correctly as specs and then be subsequently built very differently from the model. Or the spec itself can miss some critical factors and proving it just wastes a whole bunch of time.

MB: My interest isn't in offering that guarantee, but in creating a value add that diminishes the desire for a guarantee in the first place. I want to have a modeling language where the whole purpose of writing a spec is to generate a failure. Or this is the way I explained it to Hillel:

MB: What I'm really interested in is system resilience and this idea that systems have a certain amount of complexity and they have a certain amount of coupling and that it's not about optimizing for minimum complexity and minimum coupling, it's about having the right amount in the right places for the system. And so being able to sort of spec out a system so they could see where it's complex and where it is coupled, and then look at how much leeway you are giving yourself on on your inputs before the system produces an output that is not what you want. Right?

MB: So this was sort of the reason why I gravitated towards formal specification, because it seemed to have those those dynamics. And then it took me a long time to figure out 'Oh, no. The reason why its frustrating is because this language is built on the idea of mathematical correctness. On this state never being true. And I actually don't care if it's ever true.' I just want to know what are the parameters like, when will it get to that state? Like how brittle is it? And if we change it in this way, does it become more brittle or less brittle? Right?

MB: So that's sort of--there are languages that do this, but they're by and large proprietary or they're based entirely on being able to visualize systems.

MB: Wait..Wait. We're throwing around a couple of different terms that may be very foreign to you…

MB: So now the first thing that I have always wanted to know is formal specification, formal methods, formal verification, are all these terms synonyms or is there like an umbrella hierarchy between them or....?

HW: Sort of, and this is where it would have been really nice if I managed to-- I just recently moved to a new place, to get my whiteboard up and running so I could draw the little charts for you. But--

MB: This is a podcast, those little charts wouldn't help anybody.

HW: Well, it would help you understand.

HW: So one thing to keep in mind is that, like sort of any thing involved in tech, there's a lot of communities doing a lot of different things in the space... at different times. So you often see terms that sort of bubble up that certain groups use, that other groups use a different term and then sort of they get smushed together in weird ways. This is a highly broad overview, incredibly inaccurate, but it's a good enough lie to go on for now. Formal methods is just the broad field of anything involved that is called formal methods. Formal specification is the art of writing rigorous descriptions of what something should do, either what a designer should do or what specific code should do. So you write a formal specification of a design using say, TLA+ or you write a formal specification of code using, I don't know, Spark or like Idris. Then from formal verification is the art of taking the thing and taking the specification and showing they're connected.

MB: When he says "showing they're connected" the typical way to do that is to write a spec that is parsable and can be compiled into an executable model using First Order Logic.

MB: I've written about First Order Logic before, see my blog post The Subtle Power of Booleans to get up to speed, but basically you can think of First Order Logic as a puzzle using true/false statements. If A is true, and B is true, then C must be false - that sort of thing. The way this works in formal specification is that the spec defines what the system is doing and a set of assertions about states that should be impossible. So for example: here is how my system validates and approves transfers of money between accounts, check that there is no order of events that results in a negative account balance.

MB: If this sounds super impressive, I should point out that I'm actually really bad at it.

MB: ...No really, part of the reason Hillel and I became friends is because he spent so much time helping me fix silly problems with my specs when I started.

MB: I have a really hard time thinking of logic as being math. I'm exposed to it as a math concept. And then when I dig into it, I think to myself, this is kind of more like... I don't-- I don't know-- it's not fair to call it philosophy, but like it doesn't feel like math to me. And I'm wondering if I'm missing something there.

HW: Can you explain why it doesn't feel like math to you?

MB: I think because... I tend to see it as being about relationships, not about numbers, right?

MB: You know, like you have a set of certain things, do they all have the same properties, right?

HW: Are are you familiar Seven Bridges of Konigsberg?

MB: I am familiar with Seven Bridges of Konigsberg?

HW: Is that math?

MB: Uhhh...No?

HW: Ok, It's category theory math.

MB: What is Category theory?

HW: Ok, cool, we can skip that.

MB: (laughs)

HW: So this is something that I actually am very adamant because I think that there's this really weird divide in like programming where you have basically two camps essentially. You have the people who are like, we don't need math. Math is like pointless unless you work in specialist domains. The other people are like math is beautiful and shows you the underlying, like abstractions of programming and how everything is secretly a type and then how there's like-- blah, blah, blah, blah, blah. And I think that there's the third camp, which is the camp that I belong to, which is that math is directly useful to programmers in day to day life. But the problem is that the math that is sort of presented as math by both camps isn't is a very small slice of what math is, because math is fundamentally a language we've developed to explain things. And almost everything in math comes from of two places, either trying to build tools to model reality better or to build tools to model the tools that we just built better.

MB: Yeah. So I think it's less we don't do we need math or how much math to do you need to be a programmer and more... There is this cultural and psychological and emotional context around math as a subject. Right?

MB: So what you're saying before about how some people find the specifying of design unsatisfying because it doesn't connect to the code. Right. Is the design process. I think that's because people take a false sense of security in math. Right. They think like, well, it's math, ergo it's the truth. There are no opinions there. There is no subjectivity at all. It's math. Ergo, I don't have to defend myself.

HW: --I think it's... I think it's more just that you can't automatically translate it into code. You have to do that manually and then you can make mistakes.

MB: True. But like that that that goes back to it. Like, well, you could have made mistakes when you wrote the design in the first place. You probably did make mistakes when you wrote the design in the first place. But there's a feeling of like I ran it and the math proved to me. That's correct.

HW: Right.

MB: And I think there's the other side of it that people are also super intimidated by the math. And so to take something like first order logic, that is a very different fish from, let's say, algebra and and putting it under the heading of math--

HW: We're talking algebra-- for the record, just because I'm a math head-- we're talking about algebra as in like high school algebra. Right?

MB: Yes.

HW: Not like algebra as in college algebra. Ok.

MB: Yeah. As in, as in, high school algebra.

HW: Polynomial rings, algebra of polynomial rings. FINITE polynomial rings!

MB: All right. I give up. You win. I think it creates-- people self select, right?

HW: Right.

MB: People who for whom first order logic and some more concepts would be extremely valuable in the practice of their discipline avoid it because they're told that it's math and they assume that all math is like what they learned in high school that they found difficult or confusing or unpleasant. Right? And it's like sometimes I don't want to like-- if we continue this conversation much longer we're going to have to put it on Tick-Tock, because this is apparently where people discuss the philosophy of what is math?

MB: (laughs) But, it's like, I did. I do feel very strongly like, you know, why are these concepts considered math versus philosophy, for example?

HB: Well, for a long time, science was considered philosophy.

MB: Really? When did it make the switch from being something other...

HW: I think it must have been the 1880s when it-- when it stopped being natural philosophy and became science. I forget the exact details, but and for a long time, math was philosophy, too. And a lot of linguistics used to be philosophy of language, like philosophy essentially is just this big, like miscellaneous bin where we shove everything that we don't know how to classify.

MB: Well doctor of philosophy, right?

HW: This is not nice to philosophy and like rude to philosophy, but like there is not as much difference between philosophy and the disciplines that spawned from philosophy as we tend to think.

MB: My mind's been lingering on the edge of this problem. A few weeks ago I rediscovered some literature I had collected on the cybernetics movement of the 40ties and 50ties. Cyberneticians were very into modeling systems. They believed that everything could be modeled as systems of feedback loops and potentially quantified. From a modern perspective when we think of math and science as truth and human behavior as faulty, variable, inherently illogical, emotional and biased. Cybernetics seems like a pseudoscience. But this assumes that math is objective and that its precision comes from natural laws that are themselves mathematical. In other words: did humans invent math or did humans discover math?

MB: But... what if math is not infallible?

MB: For example: we cannot really accurately represent π but for most cases 10 digits is precise enough. All calculations done with π have some sort of rounding error built into them, but that never seems to matter much.

MB: In 2010 at the World Science Festival, Astrophysicist Mario Livio gave a full set of other examples:

ML: There was this astronomer, Johannes Kepler, and he made observations 400 years ago, and they were not very accurate. They were accurate for his time, but not very accurate. They were about accurate to within about four percent. Yet from those relatively scanty observations, Sir Isaac Newton managed to write a mathematical law of gravity that already by the 1950s was shown to be accurate to better than one part in a million. In fact, in an experiment done in 2008, they showed that the law inverse square law of Newton holds down to a distance of fifty six microns. One micron is one millionth of a meter. These are distances that Newton could have had no idea his mathematical law should hold true. What is it that gives mathematics such powers? We have a theory of everything that's electric and magnetic it's called quantum electrodynamics. In this theory, it's a highly mathematical theory. You know, electrons that move in atoms, they are like little magnets. You can use this theory to calculate the strength of this magnet. We can calculate the strength to parts per trillion. You calculate this magnet two parts per trillion. In 2006, this magnetic strength of the electron was measured two parts per trillion, and the two results agreed to within eight parts per trillion.

MB: What I really love about that clip is that Dr Livio talks about those things to convey the awesome impressive accuracy of math, but people like me hear it and think "...wait a minute ... so if you go smaller than that does math just stop working?"

MB: What we like to think of as mathematical laws that govern the function of the universe are abstractions that eventually break down at some point, but the point in which that break down occurs at a scale so tiny that for most of the practical applications of math the probability of it mattering is insignificant. If you throw a dart at a dart board, it doesn't matter where you hit the bulls eye, just as long as you are within the boundaries of the bulls eye.

MB: Mathematical precision is a natural process of sciences maturing. As we continue to study, we make more observations and group them in patterns. Eventually we begin expressing these patterns in math. We continue to document more observations, refining the math until it reaches a level of accuracy in which the gap between the abstraction we've created and "reality" is irrelevant. What gives math its magical quality is that occasionally the mathematicians develop the model before the reality they are modeling has been observed.

MB: In my opinion, building models looking for correctness, proofs, and guarantees is the wrong way to model. Models should be thought experiments letting us test the relationships between various abstractions so that we know where to look for real world observations for further study. But I also believe that technology suggests to its user how it should be used. If users are using modeling languages as proofs it might be because the languages themselves encourage that behavior.

HW: The biggest barrier by far to formal methods adoption, at least on a design level, is UX.

MB: Yeah,

HW: If you could improve the UX--

MB: What I find really interesting--I'm going to interrupt you for a second, sorry. What I find really interesting about UX is that it is inherently subjective, right? Like I found TLA+'s syntax to be really, really confusing and hard to grasp what it was trying to get me to do.

MB: And then hard to remember, it was like it had to be just straightforward memorization on some of this stuff.

HW: Yeah.

MB: And then I started like-- in a different train of thought for a different purpose I started learning for first order logic and as soon as I started learning first order logic I kind of went-- Oh OK, wait. Oh... I understand! I understand why the syntax is the way it is.

MB: It's like you have basically taken the user experience of first order logic and put it into a programming language. And that is why you want me to write these things the way they are. And now I understand all the errors that sort of came before.

MB: So I feel like if you were coming from the perspective of having a good foundation in first order logic and maybe some other aspects of formal computer science and/or math that you would look at TLA+ and go, oh, this is... I'm very comfortable in this medium. Where is your coming from 'I just graduated from a boot camp or I'm a self-taught software engineer and like the stuff that I'm familiar with are Python and Ruby,' you would look at TLA+ and go, what the hell is this? And why doesn't it work the way I think it should?

HW: So your basic argument is that TLA+ syntax might not be an issue. It's more of just the background you have.

MB: I think I'm arguing that there is no such thing as good UX. It's very conditional

HW: Here's my counterproposal.

MB: Yes?

HW: Running TLA+ from the command line and having the output error output as a JSON, you can pipe it to some other tool.

MB: And what would that other tool be?

HW: Well, people could build other tools, it could be something that made it easier to sort of explore. You could have it be a visualizer. You could have it be like pump it back into like a language server provider. That way you can have the errors appear in your like having errors appear in your editor. Having the ability to just like step through it step by step or drop it into a table. Like that's the UX I'm talking about. Command line tooling like better error messages-- When you get a syntax error-- in like pretty much any formal method that I've used-- The errors are always very, very like obtuse. That could be improved dramatically.

MB: Right.

HW: When I say UX I don't mean like using mathematical symbols, which I personally strongly prefer to using programmatic symbols, which a lot of programmers find easier. I'm talking about things like: not having to use the IDE, being able to script out running multiple models, bash script, things like that.

MB: OK, cool. Yeah, no, that's fair.

MB: You've been listening to Marianne Writes a Programming Language. Just a quick reminder that patrons get access to all my extras. My conversation with Hillel Wayne, for example, covered so much more ground than what's in this episode.

No One Just Designs a Programming Language (featuring Thorsten Ball)

Marianne — Wed, 18 Nov 2020 04:54:32 +0000

Summary

Marianne ponders the consequences of different design decisions and how to direct her research through an enormous amount of information and choices. Thorsten Ball, author of Writing a Compiler in Go, talks about his experiences designing Monkey and some of his regrets in retrospect. More from Thorsten Ball's can be found at thorstenball.com. Writing an Interpreter in Go can be purchased here. Writing a Compiler in Go can be found here.

Bonus Context

Become a patron to support this project.

Transcript

MB: So let's get one question out of the way, does the world really need another programming language? Probably not, no.

MB: You're listening to Marianne Writes a Programming Language, and I'm Marianne.

MB: I have always wanted to write a programming language.

MB: I figured I would learn so much from the challenge. Even 15 years into my career in technology, I feel like there are all these weird holes in my knowledge. I know a bit about abstracts syntax trees, a bit about tokens, a bit about compilers and bytecode, even a bit about logic gates. But I don't have a clear sense of how all those things work together. One thing my career so far has convinced me of is that no knowledge is useless, things I learned in the past become valuable in the most unexpected ways.

MB: The other reason why I want to write a programming language is because I can't find a language that does exactly what I want to do. If you're familiar with my work, you probably already know that I'm very interested in complex systems and models. I spent a year or two exploring formal specification, a set of tools that I still use, to be honest, before I realized that languages like TLA+ and Alloy are looking for mathematical correctness. And that wasn't what I wanted. That wasn't what I was interested in. I didn't want to know if certain problems are impossible. I wanted to know how likely certain types of problems are in a given system.

MB: I wanted to model resilience, but one thing at a time. We'll get to all of that in more detail later. So how exactly does one write a programming language? When I started this project, I thought finding a jumping off point would be easy. I typed How do you design a programming language into Google and expected to get back at least a few medium posts laying out the basic decisions. Even knowing very little upfront I had a sense that in order for programming language to work, there had to be some sense of cohesion in its design. You couldn't just pick and choose things you liked in other languages and just think it would be OK. Some things would not work with other things, but what were those critical choices? I was surprised to find not much information. I expected someone to have developed a menu of some kind--even a primitive one--to serve as training wheels for beginners, even a complete bullshit one drafted to start fights on Hacker News. I expected to be able to skim a few opinions and have a good idea of where I wanted to start researching, except I couldn't find anything like that.

MB: A theme that's going to come up a lot in this series is the incredible divide that exists between the academic world of programming and the commercial world of programming as we go down this rabbit hole together. We'll talk about completely different styles of programming, strange data types. Jesus, there's a whole world of obscure experimental languages that appear in research papers, rack up a host of citations, and never touch an actual computer other than their inventor's. At one point I asked a researcher I interviewed for this series, why do professors keep publishing descriptions of implementations without actual code? Why do I see demos of things but no source code repositories?

MB: And he told me: because they're ashamed. If they share their code, other people will find all their programming mistakes. And to me, this is a really fascinating problem. One side of this divide is developing really interesting stuff, but doesn't know how to produce mature production ready code. The other side has those skills, but finds the language of academia to be inaccessible and difficult to parse.

MB: In my search for an overview of the theory behind designing programming languages, I kept getting referred back to these thick computer science textbooks, the Wizard book, the Dragon book. You've seen them referenced as well, I'm sure. I felt like this was probably a bad place to start. Perhaps I'm reckless or just intellectually lazy, but adding a few hundred page college textbooks to the top of my reading list seemed like a good way to destroy my momentum really fast, even though without question, that was the proper way to learn. It would do me no good at all if it killed my interests. I can't remember how I found Writing an Interpreter in Go. Just one of those things, I guess. But I once I found it, I knew immediately this is how I wanted to start. I recently had started learning Go for work and I can't tell you what a relief it is to have books about general programming concepts not written in Java. Thank God. Even better, Writing an Interpreter in Go implements a programming language called Monkey, which was developed specifically for the book, which meant the author was someone who had actually gone through the process of designing a full programming language.

TB: Umm... I think you're overestimating how novel monkey is

MB: And that is Thorsten Ball, creator of Monkey, author of Writing an Interpreter in Go, and also its follow up, Writing a Compiler in Go.

TB: So I didn't set out to create a completely new programming language ... I couldn't like... no, I don't-- I wouldn't even know what it should do, but what I realized and I'm sure you've seen it now that you've dug into this, there's a ton of material on how to create program languages. And in my experience, it falls into two categories. The one category is overly academic textbook kind of stuff where it says, like, you know, it doesn't even show you what the programming looks like. It shows you only snippets and or it's glosses over the syntax and says, you know, we don't have to worry about syntax. Let's just use this lisp as a stand in whatever.

TB: And then on the other hand, you have these tutorials, posts that show how to build a programming language and they mostly show really small toy examples. And they stripped down so much. And it's often just a calculator like, you know, like a repl where you can type in one plus two when you get out three. And what I wanted was something in the middle fully documented, including tests with the real syntax, like no parentheses lisp stuff, which I love-- like, for the record, I'm a fan.

TB: But what I wanted was like the real thing, like all of the programming languages, the real ones, they have curly braces and they have keywords and whatever. And I wanted that, like, how does that work? You know? So what I basically ended up doing is writing a lisp and then putting the monkey outfit on top with the curly braces and the fn keywords and let whatever, but it's it's really similar to JavaScript in a way, in the best possible way, I guess. And JavaScript famously is also, you know, it started as a Scheme implementation, like a really small Scheme implementation .. you have-- it's immutable by default. You have first class functions. That means you can pass the lambdas around, you have higher level functions. You can return functions from other functions. Not a lot of crazy data types, no static type system.

TB: So I just took... a minimal Scheme added the curly braces and arrays and hashes and the syntax for literals, so you can like literal types, so you can type array literal or like a hash map or whatever, and that's basically it.

MB: So what were the kind of design choices that you made when you were thinking about what Monkey should look like? I mean, like not in terms of curly braces or no curly braces, but in terms of like, should it be a strict typing or like dynamic typing or should be this or should it be that? Like, how did you think about was it like you had a design phase with Monkey or was it just like I'm just going to build things and we'll see where we end up? Right.

TB: The second one, yeah, definitely. And honestly, I feel like my my brain is not built for the first type of step. It's if you start out and want to design a program language from the ground up without, you know, building it at least in a prototype-y way, I cannot think that far ahead. It's that the layer we're talking about here-- the programming language itself and the built in functions and the keywords and you know how they work together. They are so deep down.... That every little change you make has a lot of ramifications further up.

MB: Yeah,

TB: And that is the most impressive thing about programming language design. Like if you, for example, look at the Go programming language, you know, there's this whole debate about should Go have generics or not, and they Go authors famously pushed that decision in front of them and didn't want to make a decision for years or said, no, Go doesn't need them, and there's too many ramifications and effects that that would have, and people would just say, oh, can you just add this and kind of just add that? And they experimented around and had these prototypes and design concepts. And I was so impressed by.... Whenever they present it, like, oh, we make this attempt and turns out that this would result in code that looks like this or we made this and that would change Go code to be written like that. I was so impressed by their understanding of basically the power they wield in a way, because, you know, look at Go or any other language the idioms you have in a language, they just come from all of the pieces lying around, basically, like people go, oh, Go's error handling works like this. So we going to use it like that. We're going to this. This is what an error looks like. This is how we're going to use it. Ba ba ba ba ba. And if you add more pieces into that mix, suddenly the whole game changes and suddenly... you know...

TB: If you add the wrong piece, you can change how code is written in that language completely, you know? I guess Java is famous, like if you look at Java in the pre generic days when they didn't have generic looks completely different than modern Java. And the same goes to C++. Right. They added a lot of stuff. And people-- people say, you know, C++ 11 is not the same as the one from the nineties or early two thousands, whatever. All of this has ramifications.

MB: That's the thing that I think I find the most intimidating about.... like, even undertaking this, is understanding that tiny little design decisions I don't even realize I'm making could have dramatic impacts. Like I think Java six that is like the point where they changed something fundamental in how things works. And like everybody's struggling to migrate off of. Like the the Python 2 to Python 3 story like, oh, we did this wrong. We're going to do it differently so that we can grow and continue to thrive as a language. But it's going to be really, really hard to make the transition. Like, I worry probably unnecessarily, because to reach that point of success is in-and-of itself unlikely.

TB: Right.

MB: But still as a creative undertaking, you always want your work to represent the best that you can do and you never want to go "If I had only thought a little bit harder about it, I could have seen that problem coming." Is there anything in Monkey that in retrospect, if you were to go back, you would think I would have done that differently in the way it's designed.

TB: ...Yeah..... um.... I added return statements to Monkey and, you know. There's two ways to return a value from a function in Monkey. Either you add a return statement and that returns the value or it uses the last value of the last expression. Right. So if you have a small function and it doesn't take parameters, but you just put in one plus two and it returns three, this function.

TB: Or you can add, you know, an early exit and say if A > 3 return a five, closing brace and then out six or whatever, so you have an early exit and.... Those-- like those return statements, I added these like on a whim, I was like, I like the implicit return because I was used to it from Ruby, I really like it because it allows you to write these really dense small functions and pass them around... Scheme again. Return statements are not Scheme. So suddenly, once you add return statements, you break... you kind of jump into this whole paradigm and go like "Here I am!" return statements and we're just going to exit from this function early. But it doesn't really fit a lot of the other stuff and it breaks kind of control flow. For example, if-conditionals are also expressions.

TB: So if you say if true, then one else five, that whole thing evaluates to one. Right. But you can now add a return statement in the consequence order of the alternative arm of the if-conditional. And that suddenly changes to control flow because now this is not an expression anymore, but it's an expression with like a hidden control flow statement in it. And that needs to go up. Right. And then as I said, like I have first class functions, I have higher level functions. That means you can return functions from other functions. That means you can have two functions in another function and return from those two functions. Right. And this is..... I had a few bugs in there. And it's just like... it's horrible. Like it's you can make it work and it's working now. I guess there's still some bugs that nobody has found, but it's... That there was one thing where I was short sighted and I was like, "OK, I'm kind of trying to shoehorn something into this, but but I don't know what I'm doing. And now it's really hard to implement."

MB: I'm seeing more and more parallels between the task of writing a programming language and working with complex systems, I can't figure out if that's because I focus on complex systems and therefore I'm predisposed to see them everywhere. The same way a cardiologist will think of problems with your heart and a neurologist will think of problems with your brain. But it does seem to be the case that programmers create languages without being able to fully anticipate exactly how they will be used or how technology will change around them. Is the solution to this dilemma the foresight earned through experience? Should a student's first programming language be treated like the first pancake off the griddle and just thrown away? I think about the stories I've heard about the programming language C and its development, like the conventional origin story about C is that Dennis Ritchie just walked into work one day and decided to create it. In reality, the development of C started with the development of BCPL and B. Computer scientists involved in those languages would build things, then change the implementation of those languages to clear blockers they had discovered and in fact could only have discovered through using the language. C then started from all of those lessons learned and then itself had many different conflicting and undocumented implementations before it was standardized in 1982, thirteen years after its development had started.

MB: I guess, like, from the perspective of somebody who has now done this for, like... what sounds like two or three years, right? Like the first book took a year. The second book took a year...

TB: Yeah, the first book was released in 2016.

MB: Oh so like... way more than that then.

TB: I started digging into it in '15, I guess. Yeah.

MB: So like a five year journey, like if you could highlight almost like the.... the decision tree, if I can call it that, like I think there is a certain baseline level of decisions that once you have gone that direction, other things are taken off the table, like what you were saying with return statements when you decided that you wanted it to be kind of a lisp Scheme flavored language, return statements just kind of didn't fit and didn't kind of work. Like, how would you think about that in retrospect? Like, were there core decisions that stand out in your mind as "I went down this road and that took all of these things off the table" logically.

TB: I don't think I can name all of them, but a few stand out and that it won't be in chronological order.

MB: That's all right.

TB: But so as I said, like the big one was Monkey is a Scheme in disguise, right? It is a pretty simple language. It has only a few data types, first class functions. And I added the syntax on top of it with the braces and, you know, the short keywords and let statements and stuff like that.

TB: So this set. The basics, and then I realized....

TB: Once I implement that and actually, you know, wrote it down, I realized, oh, that's not really useful, you know, so I added more data types like hashes and arrays. So to make it more practical and make it more relatable or interesting, I guess, because this was always missing and once you implement an interpreter that can do binary expressions with numbers and booleans. It's cool, Yes. But it's-- it's not five hours of fun, you know.

TB: So I added these and then.... Somewhere around that time, I guess I also made a decision to not add assignments or mutability to the language. So everything's basically immutable, you cannot say that A equals 8 and then A equals 5 or whatever that is right now, that's undefined behavior ...like it's not implemented. And the reason why I did it was because that, you know. A equals eight or five is simple, sounds simple, right, but once you add mutability and you can assign stuff or reassign stuff. You also need to incorporate that in your closures which which captures state, right? Like you have a closure is a function that wraps or closes around state. So what if it closes around state like a binding of a name like A equals five? Right. When the closure is created, A equals five. And after the closure is created, you say equals eight now. You know, what does the closure return? That is a decision you have to make in different languages, have different answers to this, right?

MB: Right.

TB: That has effects like your decision. There is.. it's a simple decision to make, but it has a lot of consequences. And I kind of, you know, I avoided that decision or said it's immutable, but it also means.... It's not easy to implement loops right? Because a loop is based on a condition that changes, I guess,

MB: Right, got to increment the i.

TB: Exactly, yeah, and if you don't have a way to change something, that's not straightforward to implement. Right, like a for loop, like i = 0; i < 10; i++... That includes assignment. That includes mutability.

MB: Right.

TB: So if you don't have assignment then that's off the table.

MB: That's interesting because I would not have made that connection until you pointed it out. And like "Oh yeah. You really can't, can you?"

TB: Yeah.

TB: So I made a livestream in winter last year where I, you know, let's try out this live streaming thing. And I said, let's add loops to Monkey. And I'm not sure whether you can see it in the stream, but towards the end of it, I was like, Goddamn it, I need assignment for this. The problem is you can. You can.... you can of course, you can write like while true and then have it executed for all of eternity, right? Or you can say while My blah, blah, blah function and where blah, blah, blah function as a built in function that returns whatever, but as you know in the books everything is test driven. So we write the test first and you want to make sure that it works. And there's no good way to write a test for loops without basically-- Do like a dependency injection or mocking of the whole system, which breaks this whole idea of really short and easy to read tests

MB: Right. Right.

TB: So, yeah.

TB: And then. Yes, so there was assignments and mutability, and I also I didn't want to add classes, just aesthetic reasons, I guess, like the Scheme/Lisp py-whores were like, you know, objects are just poor man's closure and closures are a poor man's objects. So if we have closures we don't need objects, of course, readers are interested in.... how would you implement classes? But such that, again, is such a seemingly small decision that has incredibly huge consequences, like look at look at JavaScript. Like a couple of years ago to added classes and people did classes, classes in air quotes by, you know, returning objects with methods from other functions. But now that you have the class keyword and like this whole syntactic structure, for them, it changed how people write code. So it's, again, like huge consequences. And, you know, I didn't want to have classes. I'm I don't think I'm a huge OOP fan anymore, I just didn't want to have them. And also everything that I just said, I had to fit in in a reasonable amount of pages in a book.

MB: It's not a five part series then?

TB: Yeah and as you know: everything is test driven. So it's not just implementation, but it's also a test for the implementation that you need to show in the book and every bit of code. I think only two helper functions. I'm not sure.

MB: This is the place for something clicked for me. Immutable data, classes, loops, implicit returns. What we're discussing are the conflicts that arise when mixing functional programming styles with procedural* programming styles. So maybe a key part of that menu I've been looking for is about the assumptions that ground those styles. How do we want to handle state? Are functions first class? Is inheritance important?

MB: ....I think I need to get a few more books.

This should actually be imperative, not procedural but I didn't feel like rerecording that voice over just to correct that error ;)