Links - 6^th August 2023

It made me think of the different kinds of software I use and how I am willing to deal with difficult, obtuse software if it means I can get the thing I ultimately want which is often beyond the software itself. The software is often merely a means to an end.

For example, booking a flight. If there is only one flight in and out of a specific area with a specific airline, and that flight will save me time and energy and headache, I will do whatever it takes to buy that flight, no matter how crappy the website.

Or, as another example, sometimes I’ll look for something very specific online and I’ll search and search and search until I finally find it from some obscure website run by a ma and pa shop whose fulfillment system happens through individual email correspondence. Convenience falls by the wayside in contexts of scarcity.

And this idea was reiterated to us through our users. It allowed us the opportunity to rethink the kinds of projects we took on, to ask ourselves: “Is our time really best spent making this GUI wizard one step shorter? Or would we be better off doing something else for our users? Perhaps even something not software related?” It was often the latter.

As we delved further into their responses, we often found they would be much happier using things in their current state with just a few minor UI adjustments (rather than an entire UI refactor). Small quality of life fixes. And with the time we saved not building what we had showed them, they suggested we talk to the people in department X, Y, or Z and help them fix the processes which were causing them real pain.

Here we discuss, with the aid of a set of Venn diagrams, possible relationships between these kinds of side effects on the system induced by the proof, on the one hand, and those that improve the system’s security by stopping real-world attacks, on the other. At first glance one might reasonably expect the set of effects on the system induced by the proof to necessarily improve the system’s resilience to real-world attacks. As we will argue, this position is far from clear.

The area of P that doesn’t intersect A accounts for changes made for the sake of the proof that do not stop real-world attacks. These changes are side effects of the proof that don’t actually lead to a real-world improvement of security. Instead they might impose performance penalties, or restrict functionality. If the number of such changes required for a proof is large, one might reasonably question the additional cost imposed on the system by the proof process itself.

As noted, a common form of side effect of formal verification is deployment constraints imposed on a system, e.g., to reflect environmental assumptions encoded in the formal proofs or the model over which they are carried out. Often these restrictions are sensible and arguably enhance security in many scenarios. Yet for other reasonable threat models the restrictions might be overkill.

However, the more I followed the “company, team, self” approach, the more I appreciated its biggest downside. The most valuable work at a company is rarely the most interesting nor — oddly enough — what the company itself particularly values. I frequently noticed cases where engineers did the best thing for the company, solving an urgent problem with little staffing, but weren’t recognized or promoted for their work. Those engineers would slowly become deenergized and frustrated. As this pattern got clearer, it became increasingly clear to me that always prioritizing the company’s needs was too literal a solution, and a durable approach would require balancing the company’s priorities with remaining personally energized for the long-haul.

There are, of course, rules to breaking the rules. The most important being that your energizing work needs to avoid creating problems for other teams. If your fun project is prototyping a throwaway service in a new programming language, then hmm, maybe that’s fine. But if you put it into production, then your energizing detour is going to be net negative on energy generation after other teams are pulled in to figure out how to support it.

The core framework is:

1. Generally, prioritize company and team priorities over my own

2. If I’m getting deenergized, artificially prioritize some energizing work. Increase the quantity until equilibrium is restored

3. If the long-term balance between energy and proper priorities can’t be balanced for more than a year, stop everything else and work on solving this (e.g. change your role or quit)

Movies can be difficult, right? It might be tough to hold your attention, might be tough to stay awake. It can be tough to make sense of, it can be emotionally difficult to watch. Those are the ways in which it’s difficult. Passive forms of difficulty, I suppose. But it’s not what’s prized in those movies. It’s more like the thought is well, it’s worth suffering through the boredom of this movie, because the revelation that will give you, the beauty that it provides, is worth it.

Whereas in games, it’s a bit more essential to the experience. Battletoads is such an interesting classic exemplar of a difficult game because you couldn’t say, “I’m going to try to get through the difficulty in order to get the beautiful meat of Battletoads.” It’s not the hard part around a succulent meat. People are playing Battletoads for the part that is difficult. Nobody’s in it for the graphics anymore. Nobody’s in it for the storytelling or the characters. It’s the gameplay.

I wanted to do something like that in the text. So the idea was, “What’s the experience meant to be?” The experience of playing Getting Over It is meant to be that you strive to make progress. And then you lose some and you feel that frustration, that loss intensely. You meditate on what that’s like to overcome that. I want to give you that as the experience. I know not everybody wants it. That’s totally fine. But it’s not an accident that it’s coming out that way, right? If I’ve only played real progress-forward games like JRPGs or Ubisoft open-world games where you really can’t lose progress at all, and then I come into this and it’s not framed for me, I just think it’s broken. I’m like, why doesn’t this have save points? Why doesn’t this have quick reload?

If you want to have a game that has lost progress, that has to be conveyed to the player, they have to understand that that’s part of the point. And so in a way everything about Getting Over It is about conveying that to the player. The marketing is like that. The script is like that. The presence of the author is like that. The fun here, the enjoyment, the meat of the experience is in losing progress. And I think that worked. I mean, I think people got it.

I’ve been playing a work in progress game by some friends recently that’s very difficult. I’m looking inward on this experience of playing it. This game is a really good choke machine. Games can make you start to tilt and become self-conscious and to choke. Getting Over It is an excellent choke machine. You can take somebody who’s normally very calm and very clutch. If they practice something then they can reproduce it perfectly. But there are certain ways that you can create an experience that brings people more to that level of like, “Am I actually gonna be able to do this? Now I’m starting to tilt — Oh, fuck, now I’m tilted. Now I can’t do it at all.”

Overwhelmingly introductory database materials focus on the iterator model, but modern systems, especially analytic ones, are starting to explore the push model more. As noted in the Shaikhha paper, it’s hard to find apples-to-apples comparisons, since a lot of the migration to push models are motivated by a desire to compile queries to lower level code and the benefits that come from that cloud the results.

CastleDB is used to input structured static data.

Everything that is usually stored in XML or JSON files can be stored and modified with CastleDB instead.

For instance, when you are making a game, you can have all of your items and monsters including their names, description, logic effects, etc. stored in CastleDB.

CastleDB looks like any spreadsheet editor, except that each sheet has a data model.

The model allows the editor to validate data and eases user input.

For example, when a given column references another sheet row, you will be able to select it directly.

CastleDB stores both its data model and the data contained in the rows into an easily readable JSON file.

It can then easily be loaded and used by any program.

It makes the handling of item and monster data that you are using in you video game much easier.

A modern 2D level editor from the creator of Dead Cells, with a strong focus on user-friendliness.

I’m about thirty-five years into Unix shell programming now, and I continue to despise it. The shell’s treatment of whitespace is a constant problem.

Routinely, when faced with programmers who want power at all cost, language designers think “I know, I’ll add macros!” Now they have infinite problems.

…

The correct answer is: quit your job, it’s not worth it, life is worth living, save yourself! Friends don’t let friends design languages with macro systems. We’ve made things more powerful, but we’ve lost really important properties that may well be much more useful. But more importantly, I think this decision is routinely made without understanding these consequences.

I could probably go on about programming languages: C++ and Scala both seem like dumping grounds for designs that are the product of “but then we can’t do X, so let’s make this even more powerful…” So let me pick a smaller kind of language: tiny DSLs or configuration file formats.

It’s a frequent occurrence that these start off as small declarative languages, and then as they evolve, they end up accidentally becoming Turing-complete. Generally, to their detriment. Sometimes, people advocate deliberately confronting this problem from the beginning: start off Turing-complete, just base your format on Lua or embed the DSL in Ruby or Haskell or something. That way, you’re not reinventing a general-purpose language, badly.

But… there’s still good reason to want your configuration format or DSL to be declarative. It goes from being data you can analyze to code that you have to execute. (Among a great many other things, imagine trying to deal with a file from an untrusted third party.)

One trick you can use to try to avoid this fate is to separate out automation from declaration. Encourage (and build tools to support) programmatic generation of the declarative file. Any time someone wishes they could write arbitrary code in the file, they may instead be able to write that arbitrary code to generate the file instead. This works surprisingly often, in my experience.