What happened to Mark Brendanawicz?

Mark Brendanawicz was a character on NBC's Parks and Recreation for seasons 1 and 2. Before I get into any detail, I wanted to settle something...

What is up with that surname?

I don't know a ton about Polish names (Leslie refers to Mark as Polish in season one), but "Brendanawicz" sounds like a made-up name, like someone was making fun of a guy named Brendan at a party, forgot his last name, and ended up referring to him as "Brendan Brendanawicz." I found a website where you can check whether a name is in the top 150,000 names in the 2000 census. Here's what I get back on Brendanawicz:

As a point of comparison, I queried the surname of a long lost friend from high school:

That's only about 30,000 from the bottom! And now someone I knew at Brandeis:

This is clearly not scientific, nor is it even pretending to be conclusive. Anyway, I guess appearing in the top 150,000 surnames is a bit of a wash. I still think it doesn't sound real.

The real point of this post

Mark begins the show as kind of a playboy and a bit of an ass. When he begins dating Ann, he starts to act less selfish and actually comes across as a good guy. In fact, he just keeps hitting home runs in the good guy department over the course of season two. Here are some reasons why Mark actually turns out to be a good guy:

• Rather than behaving territorially, he shows compassion toward Andy (Ann's ex), who still hangs around, expecting Ann to take him back.
• Unlike Andy, Mark understands that Ann is not a prize, but a person. He doesn't ever try to assert control over her, and he never stoops to the sitcom stereotype.
• Rather than purchasing something useless and typical for Ann's birthday, he buys her a computer case. She had mentioned many weeks before her birthday that she needed one. He listened to what she was saying, wrote it down, and waited to surprise her with one.
• He makes fun of himself. On Valentine's day, he dresses up and enacts all of the cliches, giving Ann a Teddy bear, chocolates, roses, etc., because he's never been in a relationship with someone on Valentine's day. Ann is not dressed up, she's hanging out on the couch, and she's just enjoying his company.
• When Ann fails to introduce Mark as her boyfriend to a childhood friend she's always had a crush on, Mark doesn't get jealous, confront her with it, or otherwise act super dramatic. He has ever right to be hurt -- it was a glaring omission, and her feelings for this friend are obvious. However, he deals with it with grace, even going so far as to talk to Andy about it.

What I appreciated about Mark was that he was a good guy who, despite never having been in a serious relationship before, knew enough about human interaction to treat Ann like a person, and not just TV Girlfriend Stereotype. They had one of the healthiest, most respectful relationships I've ever seen in t.v. Sure, the way the writers began their relationship was kind of shitty, but somehow Ann and Mark worked.

The way they portrayed Mark contrasted with Tom Haverford, who thinks he's starring in Entourage (a show I've never seen), or Ron Swanson, the manliest man or something. Tom hits on women so aggressively, but with such little tact and appeal, that he's turned himself into a joke (a joke who should also be disciplined for sexual harassment on a regular basis). Yeah, his character is funny, but what he does is NOT OKAY. Ron Swanson is Teddy Roosevelt, constantly performing masculinity. He's also quite entertaining, but definitely a caricature.

I very much enjoy watching both Tom and Ron, but having Mark balance them out is a rare treat. You just don't see men behave with such grace, maturity, and self-respect on t.v., without being...well, Captain Adama.

Formal Methods in Practice

Emery recently sent me a link to an experience report of a collection of engineers at Amazon who used formal methods to debug the designs of AWS systems. It's pretty light on specifics, but they do report some bugs that model checking found and discuss their use of tools. They describe why they turned to formal methods in the first place (hint: it wasn't a love of abstract algebra and proof by induction) and how they pitched formal methods as their solution to a variety of problems at Amazon.

SAT solvers vs...Something Else

The report begins by noting that AWS is massive. As a result, statistically rare events occur with much higher frequency than the [human] users' gut notion of rare events. The first anecdote describes how one of the authors found some issues in "several" of the distributed systems he either designed or reviewed for Amazon. Although they all had extensive testing to ensure that the executed code would comply with the design, the author realized that these tests were inadequate if the design was wrong. Since he was aware that there were problems with edge cases in the design, he turned to formal methods to ensure that the system was actually exhibiting the behaviors he expected.

His first attempt at proving correctness of these systems was to use the Alloy specification language. Alloy's model checking is powered by a SAT solver. At a high level, SAT solvers model many states of the world (i.e., a program or system) as boolean propositions. If we wanted to talk about a distributed system, we might have propositions like MasterServerLive or PacketSent. These propositions have true or false values. Nothing that isn't explicitly defined can be described.

If you are familiar with propositional and predicated logic, this should all be trivial! However, if you're not, you might be wondering what we mean by "nothing that isn't explicitly defined can be described." Consider this: I have 10 computers from 1995 in my basement. I split them into two clusters. Each has one queen and four drones (1). I'd like to state some property foo about each queen. Since I have two queens, I would have two propositions: FooQueen1 and FooQueen2. If I never need to use either of these propositions separately (that is, if they always appear in expressions looking like this: $FooQueen1 \wedge FooQueen2$), then I can just define one proposition, $FooQueen$. If, however, I want to say something like "foo is true for at least one of the queens," the I would need each of FooQueen1 and FooQueen2.

Every time I want to assert some property of these two queens, I will have to create two propositions to express them. Furthermore, if I want to say something we'll call about a relationship bar between a queen and each of its drones, I will have create variables BarQueen1Drone1, BarQueen1Drone2, ..., BarQueen2Drone4. Any relationship or property that isn't described in this way cannot be reasoned about.

Anyone who has experience with first order logic might point out that there is a much more elegant solution to propositional logic -- we could always just describe these properties as predicates over a universe. Instead of defining two propositions FooQueen1 and FooQueen2, we could say $\forall x \in \lbrace computers \rbrace: Queen(x) \rightarrow Foo(x)$, which states that if one of my basement computers is a queen, then foo holds. This expression gives us the possibility of adding another queen to the system without having to explicitly add more propositions.

So far so good, right? Well, there's a another problem with using SAT solvers for distributed systems -- timing information matters. Some processes are redundant, and we need a way to describe concurrency. We could try to define predicates like Before and Concurrently, but again our model explodes in the number of "things" we need to specify. Tools like Alloy have no notion of timing information -- we have to tell it what temporal ordering means.

The author found that Alloy simply was not expressive enough to describe the kinds of concurrency invariants he needed. He instead started using TLA+, a modelling language based on temporal logic, with logical "actions" (I think I learned about this in a class I took on logic in NLP, but I don't recall much about it and the Wikipedia page is empty). This language was expressive enough to describe the systems he wanted to model. Others at Amazon independently came to the same conclusion. Some found a language on top of TLA+, called PlusCal more helpful.

Prejudice

There seems to be a lot of suspicion (if not prejudice) in the "real world" of formal methods. The authors decided to market their approaches as "debugging designs," rather than "proving correctness." This part was the real hook for me. I'll admit, formally proving things can be quite satisfying. Proving correctness or invariance can feel worthy in their own right. Unfortunately, not all problems may be worthy of this effort.

A major problem in the adoption of these tools is that they aren't marketed to the right people in the right way. Pitching formal methods as a way to "debug designs" has a lot of appeal to pragmatists -- it emphasizes the idea that designs themselves may be flawed, and these flaws may be difficult to find. The authors cite medical devices and avionics as fields that value correctness, because the cost of bugs is very high. However, in most software systems, the cost is much lower. A bug that hasn't been exposed in testing is probably quite infrequent. Its infrequency means that the cost of paying someone to ensure a program's correctness outweighs the cost of the consumer's exposure to the bug. What the authors realized, and what they pitched in this paper, was the idea that an event that only occurs 1 out of a billion executions is no longer a rare event in real software systems. There is a mismatch between the scale at which we test and develop and the scale at which we run production code. We may not be able to extrapolate that a program is correct or a system robust to failure on the basis of testing that are orders of magnitude below actual load.

How this relates to me

Our pitch for SurveyMan and related tools is similar to the authors' pitch for using formal methods for large systems. We're starting from the assumption that the design of the survey (or experiment) may be flawed in some way. Rather than deploying costly studies, only to find out months or even years later that there were critical flaws, use formal methods instead. Our tools don't look like formal methods, but they are. We construct a model for the survey on the basis of its structure and a few invariants. We use this data to statically analyze and help debug the results of a survey. The author's model checking and our random respondent simulations are both used to check assumptions about the behavior of the system.

Footnotes

1. Technically, the "proper" terminology here is master/slave, but that has an inhumane, insensitive ick factor to it, so I've decided to start calling it a queen/drone architecture instead.

When the needs of the few outweigh the needs of the many

I'm not posting much these days, since I'm currently in California on an internship. I have some posts I'd like to make on notes from the summer, but posts will likely being sparse for the next few months.

However, I'm up thinking about something and thought I'd blog about it.

The facts

A few days ago I received an email from a TA at Prestigious Institution X, asking me to take down my Software Foundations github repository because students were allegedly taking too much "inspiration" from it. My repository contains solutions to a chunk of the textbook, painstakingly solved mostly by me, with some input from Cibele Freire, logician. Posting solutions to a textbook released under the MIT license is, I believe, quite legal. Using those solutions to cheat in a class, however, is typically against an academic institution's honor code. Since there is no course even remotely similar to this at UMass (and in fact, few other resources exist to bootstrap a self-study plan for learning Coq and formal verification), I do not believe I am in violation of UMass' code of student conduct. The email implied none of these things, but I wanted to make sure I wasn't doing anything illegal or malicious in ignorance.

The academic world is a small one, so I consulted with my advisor. He suggested that I email the folks teaching the class, explain my reasons for having a public repo, and offer to make the repository private. The response to my email was indeed a request to make the repository private. I'm putting the previous link to the repository in this blog post, just in case someone comes searching for it and Google happens to index this post:

http://github.com/etosch/software_foundations

If you would like access, please email me directly. I am happy to discuss problems and give people access when it is appropriate to do so. There are plenty of exercises I have not completed, but would like to. I expect anyone who is interested enough to email me to abide by their school's honor code, if applicable.

The principle of the thing

Me taking down my repository does not dissuade cheating. It just buries cheating a little deeper. Dishonesty and plagiarism are pandemic in computer science. This shocked me when I started working in CS. In the humanities, the standards for attribution are quite explicit and stringently applied. Students must routinely attend lectures on academic honesty. I have never seen seen anything even remotely similar in computer science.

Removing the repository from public view shifts the blame from the student plagiarist to the provider of information. At one point in my life, when I thought I would go to grad school for English Literature, I made writing samples publicly available. Would I be culpable for someone plagiarizing my work simply because I wished to promote my work? No one would ask Harold Bloom to stop publishing if a student plagiarized him in a Shakespeare class. Obviously I'm no Harold Bloom.

The perpetrator (plagiarist) here is the one in the wrong.

It's a bit difficult for me to not be personally a little upset/frustrated by this. Not only does it devalue work in our field, but there's something maddening about students at Prestigious University X ruining it for the rest of us. I doubt they think that way, and I doubt anyone would ever put it to them that way. One of the earliest courses I took in computer science was SICP. It was not taught well. Coming from the humanities, where you actually do the reading you're assigned, I read the text. I also did nearly all of the exercises up to the chapter on metacircular evaluation. This self-study was extremely important to my education. When I got stuck on a problem I couldn't solve, I searched for the answer on the internet. Seeing solutions from people who were better programmers than I was made me a better programmer.

Eventually someone else will post solutions and it won't matter much that I took mine down. My solutions are still cached out there and I know some rando forked my repository. A quick search of github for "software foundations" and Coq returns about 80 results and at least one looks fairly complete.