Author Archives: david

Taking (Part Of) My Self Offline

Context: I’m working through some things at the moment. As I do I will try to share parts of it that I think will be useful to other people, but these will still be somewhat personal and will be heavily redacted.

Epistemic status: My understanding of both addiction and the mind are at best simplified, at worst may be very flawed without my realising it, but the conclusions still seem to be useful for me.

Attention conservation notice: 90% problem framing, 10% solution. Skip to the end if you just want the idea.

Hi, my name is @DRMacIver, and I’m addicted to Twitter.

I know there’s a lot of moralising panic around internet addiction, and I don’t want to feed that, so let me just state outright: I’m not here to judge your Twitter usage. Mine is on the high side, and when I try to correct that it tends to revert to its previously high state after a short while, and I don’t like that. Your Twitter usage may be fine for you.

I don’t think the comparison is unwarranted though. Twitter is basically a Skinner box.

The only other addiction I have struggled with is caffeine (my flatmate jokes about my struggles with the mildest addiction in the world. Though I think this underestimates how bad caffeine addiction actually is, I’ll certainly grant that it’s not up there with a lot of the more serious ones).

These feel pretty similar from the inside – there is a gap between the state I want to be in and the state I am in, and closing that gap requires a state of constant willpower even after I’ve seemingly fixed the problem.

Addictions in general seem to have at least two parts: The inherent addiction, and the problem that you are using the addiction to solve. It’s not that the rats in the rat park don’t get addicted, but because they don’t have the problem of social isolation that the rats in the cage are solving with drugs, they are able to wean themselves off it.

This has been my experience with caffeine. Previously when I quit caffeine I would get through the initial awful couple of days, the merely crap week or two, and then I’d no longer be addicted to caffeine.

I’d also be exhausted all the time. As well as being an addiction, the caffeine was something I was using to self-medicate, and without it the problem that I was using it to solve came back. I didn’t like being exhausted all the time, so I inevitably started drinking caffeine again.

I don’t have a caffeine addiction these days. Sometimes I drink caffeine. Occasionally I do so often enough in a row that I accidentally re-addict myself, and then get mild headaches when I stop. It’s mostly fine.

Once I mostly sorted out my sleep (thanks, nose surgery) and found some medication that worked better for me than caffeine (sorry, this is one of the redacted bits. Talk to your GP and/or dodgy grey-market internet pharmacy, but obviously I cannot condone the latter option), I managed to get my baseline up to “kinda tired but mostly functional”, which seems to be good enough that I don’t automatically fall off the caffeine wagon.

So what’s the equivalent for Twitter? What need is the addiction fulfilling?

Well, uh, I made a list. It has eight items on it, in roughly three different categories. Turns out that it may be a tire fire hellsite hot take machine, but it does seem to fulfil some genuine needs in my life.

Most of that list is on the redacted pile (I may write about some of it later), and some of them are probably unsolvable without solving massive coordination problems, but one thing stood out as worth sharing and actually solvable. It’s also a problem that is worth solving in and of its own right, even if it doesn’t make a dent in the addiction: Twitter has become a place where part of my extended mind lives, and that’s not a great idea.

I don’t know if you’ve noticed, but trying to think things through bare-brained is terrible. Try just sitting there, closing your eyes, and thinking through a problem. Even if you’re one of those weirdos who can paint imaginary pictures on the back of your eyelids, there’s a really hard limit to how much you can handle on one brain alone. Even if you have a much better focus than I do and can actually keep yourself on track, your working memory is only so large. Mine is pretty good I think, but I still very rapidly hit my limits when solving complex problems.

The solution of course is to stop trying to think with just your brain. Maybe this is more obvious if you’ve trained as a mathematician, I don’t know – certainly a lot of why this is obvious to me is that the idea of trying to prove a theorem without writing it down as you go is basically laughable for most of us. A mathematician with a pen and paper is an infinitely more capable creature than a bare-brained mathematician, because their working memory has expanded enormously.

It goes beyond that of course. We think of language as the tool to explain our thoughts, but that’s mostly nonsense. Language is as much a tool for thinking as it is a tool for communication – there’s a reason why explaining yourself to a rubber duck is such a powerful technique for understanding things.

So how do you expand your intelligence? Using a tried and true method: You write it down. Suppose you have a thought and you go “Hmm there’s something there”. Even if you don’t care about capturing it, writing it down will significantly help you expand on and flesh out the thought.

So, as my mind buzzes away throughout the day (honestly, damn thing won’t shut up. I’m working on it), a thought surfaces, I want to expand on it, so I write it down.

Well, Twitter, obviously. It’s the most readily available medium for short ephemeral pieces of text that I want to think through. I’m already using it, and there’s a little text box I can just write stuff down in right there.

This seems like a bad life choice, even independently of the general desire to reduce Twitter usage.

As well as resulting in a rather noisy timeline (I have several friends who have unfollowed me because they couldn’t deal with the volume. Sorry), it also has an unpleasant shaping effect – I don’t want to be a person who is only able to think properly about things that are expressible in publicly visible 280 character chunks. A lot of things I think about do not fit into that category, either because size, personal nature, or any one of a number of other things that would make just really not want to share them on Twitter.

Anyway, i don’t know how to solve the Twitter problem more broadly, but this one I can solve.

Like I said, I’m working through some things at the moment. One way I’m doing that is by making use of that extended intelligence I talked about above by writing about the problems that I am trying to solve, by hand, in a physical journal. This has proven pretty helpful in an occasionally-terrifying sort of way.

I would like to keep doing this, but my track record with keeping journals is pretty poor, as is my track record with forming a habit of doing difficult things.

So, to recap, I have:

A compulsive habit of writing down my thoughts in a place that I would like to stop using for that.
A place for writing down my thoughts that I’m worried that I’m not going to use enough.

Yeah I don’t see the connection either. Maybe if I stare at it a bit longer.

Anyway, so that’s what I’ve been doing over the last couple of days. When I feel the desire to tweet to think through something, I (usually) write it down in the journal first. If I still feel the need to tweet something about it, I can, but the journal is the place where thoughts go to form, and Twitter is where I share them.

We’ll see if I keep this up. It’s looking pretty good so far, but things usually do for the first week or so.

Anyway, that’s it. No snappy conclusion to tie all this up, sorry. Just a thing I’m trying – It might work, it might not, but I thought I’d write it up now while I was getting started and the idea was reasonably fresh.

Monads as an interface for composition

Fair warning: I’m going to be talking about monads. It’s in the title and everything. This post is even a little bit of a monad tutorial, as I’m not going to assume that you know what a monad is, though that’s not the main point of it.

A thing I’ve been thinking about recently is that a lot of the success of QuickCheck and descendants as a way of getting people who are not testing specialists to use better testing techniques comes from the fact that random generation is a monad (QuickCheck’s use of it technically isn’t a monad, but the difference is unimportant enough that I can elide it for this post. You could fix this problem and literally nobody would notice).

A point in favour of this theory is that even though Hypothesis has abandoned normal random generation as its underlying method, it’s done so in favour of adopting a different monad (monadic parser combinators, if you’re curious).

Fundamentally the thing that makes QuickCheck so effective is that it is providing a library of composable data generators – you can take existing generators and turn them into generators for lists of that value, apply functions to them, etc.

This makes it extremely easy to define generators for your own data types, and the reason you can do that is fundamentally that the composition interface is the monad one.

When you first encounter Haskell you see something like the following:

main = do name <- getLine
          putStrLn $ "Hello " ++ name

And OK you might think it looks a little syntactically strange, but it basically looks like a normal program, and it’s only when people tell you that there’s something called a monad involved that it starts to seem like anything strange is going on.

But the first intuition is correct: Nothing strange is going on, and this code really does do the obvious thing (there’s a little bit of non-obviousness for people in terms of the difference between “let x = y” and “x <- y”, but I’m going to ignore that). It really is “a normal program”.

The thing that is unusual is not this program, but the fact that it is an instance of a more general one.
Suppose you instead had the following:

sayHello get put = do name <- get
                      put $ "Hello " ++ name
 
main = sayHello getLine putStrLn

And now we have this split into two parts, with some code that is abstracted over how you get and put the name (maybe you want to run this as part of a website as well as a command line? I don’t know. It’s an artificial example. Bear with me here), and a main definition that calls that abstracted function with concrete implementations for terminal I/O that read and write lines.

This is all type inferred, but lets be explicit about the types:

sayHello :: IO String -> (String -> IO ()) -> IO ()
sayHello get put = do name <- get
                      put $ "Hello " ++ name
 
main :: IO ()
main = sayHello getLine putStrLn

So sayHello takes one argument that is an IO String (“an effectful program that returns a string”) and one argument that is a String -> IO () (“a function that takes a string and does some effects”), and main just passes the corresponding values to it for our command line program. This is just extracting a function from our original program, business as usual except that because it’s Haskell we have a specific type for “things that have effects” and we have all the usual higher order function goodness.

Where monads come in is the observation that we’ve actually used nothing about IO in the definition of sayHello – all we’ve used is do notation and strings, so we could abstract it to anything that supports do notation, which is precisely the monad interface.

sayHello :: (Monad m) => m String -> (String -> m ()) -> m ()
sayHello get put = do name <- get
                      put $ "Hello " ++ name
 
main :: IO ()
main = sayHello getLine putStrLn

This is exactly the same program, all we’ve done is generalise the type signature for sayHello to only use the operations it requires from IO rather than the full complexity of the IO type.

(You could make this type signature more generic yet by replacing () with a type parameter, but I think the concrete version is clearer for explaining this point).

So that’s all that monads are: The type signature for things that support do notation (plus some laws that ensure do notation behaves reasonably sensibly), and do notation just looks like normal programs.

So what are monads? Well they’re a monoid in the category of endofunctors err a type class with the operations return and >>= satisfying the laws no basically a burrito in a space suit actually never mind it doesn’t matter what monads are, but the reason why monads are useful is that they represent data types that you can compose together with do notation, and do notation looks basically “like writing normal programs that return values”, which is extremely convenient because we can build on our normal experience and intuition about writing such programs.

That’s not to say monads are normal programs that return values, only that we can build them up as if we were. e.g. a monad might “return” no values. e.g. suppose we ran the above code with the maybe monad:

main :: IO ()
main = print $ sayHello Nothing (\_ -> Just ())

This takes our existing sayHello function but the get argument always fails (returns Nothing) and the put argument just returns () without doing anything (because the only things it could do are either that or fail). This program now prints the string Nothing, because rather than ever “returning a value”, instead the computation “failed”. You could think of this as saying that normal programs with exceptions also compose like monads. Similarly a monad might “return” multiple values (e.g the list monad), do backtracking (a parsing monad), or many other things.

What any given monad actually does can be almost arbitrarily complicated, but the monad interface isolates us from that by allowing us to compose them together as if they were such programs anyway.

In QuickCheck this comes in by letting us compose generators together easily using do notation:

integerRange :: Int -> Int -> Gen Int
integerRange = undefined -- Imagine we had a real implementation here
 
 
orderedPair :: Gen (Int, Int)
orderedPair = do a <- integerRange 0 10
                 b <- integerRange a 10
                 return (a, b)

The access to do notation means that these generators compose more or less how we’d expect programs to without us having to have any knowledge of the underlying implementation or source of randomness. Or even how these will be run – in QuickCheck, Gen more or less is just a program that returns a random value, but e.g. in Hypothesis one of the possibilities of drawing is that it may fail because it violates some assumption or is unable to generate a good value, and that can just as easily be rolled into the monadic interface.

Python doesn’t have do notation for monads, but it does have free side effects, so in Hypothesis we use the @composite decorator instead of do notation, but the motivation for that was absolutely “Boy I wish there was a way to compose Hypothesis generators that was as easy as do notation”.

But if we don’t have do notation, what does it being a monad buy us?

Well, directly not much. Oh, sure, if you have monads as a first class concept in your programming language, you can define a whole bunch of useful functions that take generic monads, but they’re not that useful. They’re nice to haves. You can just write the special case version in a couple of lines if you really need to.

But even without do notation, it’s not too hard to use the monadic interface. We could write the above as

orderedPair = integerRange 0 10 >>= \a -> (integerRange a 10 >>= \b -> return (a, b))

This does the same thing as the do notation, and it just uses more explicit chaining. It’s unwieldy, but people have shown themselves perfectly able to translate the sort of normal program composition reasoning when writing promises, and before I added @composite to Hypothesis people were happy to use flatmap (which is the Hypothesis equivalent of >>=), and this is no different just because it’s not tied down to a specific monad implementation.

Even if you never consciously express the fact that your data type is a monad and can’t represent it in your programming language, the fact that it is one still puts it in a particular corner of the design space, and it’s a particularly attractive one because of how easy monads are to use.

This ease of use is then a lot of what has enabled the popularity of QuickCheck – because it’s so easy to define generators for your own data types, people can and do, and this then enables QuickCheck to be used in so many contexts.

It’s also what constrains QuickCheck to being a particular local maximum I think. Ensuring the monad property is hard, because many natural operations do not compose monadically. Shrinking is an example where the natural composition is not monadic – it doesn’t compose like a normal function, because you have to be able to “reverse the arrows” – to turn a Shrinker a into a Shrinker b, you need to be able to transform both from a to b and from b to a, and monadic composition isn’t bidirectional like that. test.check and Hypothesis both build shrinking into the generation to make it monadic (though test.check struggles with actually making the monadic composition shrink well).

The way Hypothesis escapes this is by building in some of these operations at a lower level. Instead of operating in a monad representing a random number generator, it operates in a parsing monad. In a parsing monad, “running” the monad corresponds to reading some bytes of input and either failing with a parse error or returning a value (possibly multiple values if you want to handle ambiguity). Parsing monads are neat and you can see a proper example of them in things like parsec, but Hypothesis gets to be relatively simplistic in its implementation of them because it doesn’t have to do anything like back-tracking.

The reason you can use a parsing monad for this is because non-determinism is a form of parsing: A pseudo-random number generator is basically “just” an infinite stream of bits, and consuming those bits to get non-determinism is just parsing the stream. You can then extend this to a monad which parses finite sequences of bits by having the parse fail if you ever read try to read past the end of the sequence. Shrinking in Hypothesis then becomes a matter of trying to minimize these finite input bit sequences in the shortlex order (first minimize the length, then minimize lexicographically. The latter lets us do things like shrinking integers towards zero). This lets us escape this local maximum by basically avoiding all the hard parts of composition: We just need to be able to construct a value, and all of the things that we manipulate are of a single concrete type, so we never need to do the reverse transformation back into the original type because shrinking isn’t operating on values at all, just on the underlying representation that is being parsed.

One of these days (hopefully soon) I’ll publish a paper expanding on that, but that’s just a taster and not the important part of this post. The important part of this post is that the public interface of Hypothesis and QuickCheck being a monad gives them very powerful composition properties that makes them much easier to use.

If you’re not writing a fairly general purpose library, you probably don’t need to understand this (not that you shouldn’t try, you just don’t need to). Just use the monadic interface and don’t worry about it too much – people are doing this all the time with specific things that happen to be monads and it works out great for them.

But if you are writing a fairly general purpose library – promises, test-case generation, etc. then the question “Can I make this type a monad?” seems to push you into a particularly useful corner of the design space, because it enables users to build instances of your type in a very pleasant to use way.

Trashy Fiction Recommendations

I would be the first to admit that my taste in fiction is lowbrow. It’s the fairly classic nerd pattern of mostly reading genre fiction – it used to be mostly sci-fi, these days it’s mostly fantasy (I’d like to read more sci-fi, I just don’t often find new sci-fi authors I actually like these days).

But there are still a lot of really good works within those genres, and I try to make sure I read those. e.g. I strongly recommend everything from Among Others onwards (I’m not such a fan of her early work) by Jo Walton because I think she’s genuinely an incredible writer.

If you look at past book recommendations you might get the impression that that’s most of what I read. This is, uh, not the case. I have a Kindle Unlimited subscription for a reason, and that reason is not that there are a lot of hidden gems lurking in Kindle Unlimited.

So here’s a collection from the other side of my reading list: Stuff that is a lot of fun but that I would be hesitant to call good, or that I have to apply some serious caveats before recommending. Many of these are in some significant way Problematic.

(Side note: There’s an interesting gender reversal that I don’t entirely understand – most of the books I read that I think are actually good are by women, and my normal recommendation lists reflect that, but most of the books on this list are by men. I don’t really know why this is, though I have some hypotheses that I won’t go into here).

Apologies to any authors who feel slighted by their inclusion on this list. I really do enjoy your work.

Niall Teasdale

Would you like to read literally dozens of books with a variety of interesting, well-developed, characters from a large cross range of genders and sexualities, with a decent (if not amazingly well handled) range of races and cultural backgrounds? The characters are enjoyable, the world-building is top notch, the plots are engaging, and the books are generally a huge amount of fun.

You would? Great. Oh by the way it’s basically porn. And not especially good porn.

Niall Teasdale is a frustrating author for me in this regard because all of the above is true. I really do enjoy most of what he writes, but there is a very specific pattern where the protagonist is literally always a bisexual (often originally straight but made bisexual through magic and/or science) woman who has a great deal of sex which he describes in detail. If that’s either your thing (remembering that it’s written by a presumably-straight guy) or you are able to overlook it, his work is a lot of fun.

Mother of Learning

Mother of Learning is about a pair of wizards caught in a month-long groundhog day loop.

It’s pretty well written, but violates my rule against reading wizard school books (wizard school is a lazy excuse for infodumping) and my preference against extended battle scenes (lazy filler to make up the word count without having to include actual plot). Also a lot of the appeal is basically watching the endless grind of power up.

On the other hand it has an adorable giant spider named Enthusiastic Seeker of Novelty, so it has that going for it.

It has a fairly major tone shift midway through, and I kinda liked the early half better but I’m still enjoying it.

With This Ring

With This Ring is a self-insert fixfic where the protagonist gets stuck in the Young Justice universe (DC animated series. Highly recommend the series regardless of whether you read this) with an orange power ring. For those not familiar with the DC cosmology, orange is the light of avarice. His ring gives him power to achieve his goals directly in proportion to how much he wants those things, with the unfortunate side effect that he has to constantly work to not be overwhelmed by greed.

He sets about trying to address the question of “If you all have this amazing tech, why are you using it to fight bad guys instead of fixing the world?” among other things. One of this first uses of the orange power ring is to go about fixing the great pacific garbage patch, and at some point he starts using freeze ray technology to start repairing the polar ice caps.

Most people I’ve recommended it to do not like it. There are a lot of problems with it e.g. the author’s politics are somewhat objectionable in places and it shows through in the fiction, and the protagonist becomes increasingly hard to relate to in fairly disturbing ways as the story goes on.

I think some of the appeal for me is definitely the daily updates. It turns out that I’m willing to overlook a lot of flaws for daily updates. Beyond that, I enjoy the fix-fic aspects of it quite a lot – both the attempt to give the DC universe a semi-coherent cosmology and also the fantasy of using super powers to actually try to fix the world.

Worth the Candle

Have you encountered the genre of LitRPG? If not, I recommend this piece about it.

The short version is that LitRPG is a genre of fiction in which game mechanics play an explicit role. Characters actually have levels and gain XP and are aware of it in world. Often, but not always, LitRPG is also portal fantasy – the protagonist has found himself (gendering intentional – LitRPG is overwhelmingly male) transported into a world that is somehow also a game. Often but not always it ends up with a harem fantasy on the side. What you are imagining about both the target audience and the typical authors right now is unkind but probably not unfair.

Most LitRPG is unreadable trash, but occasionally LitRPG is readable trash.

Worth the Candle is the only one I’ve encountered that I would say is actually pretty good. The protagonist is a rather bitter teenager who finds himself in a world that has a disturbing resemblance to a lot of the D&D campaigns he has run, including some of the darkest aspects of it that he wrote when he was going through a rather bad point in his life.

I don’t know how much you will get out of this if you haven’t had some prior exposure to LitRPG as some aspects of it are explicitly deconstructions, but I think the story stands on its own.

If you want examples of LitRPG in its raw undiluted form, I can “recommend” The Arcane Emperor (which is terrible, but I somehow still read 80ish chapters of before giving up on). There’s also “My Trans-Dimensional, Overpowered Protagonist, Harem Comedy is Wrong, as Expected“, which is a rather strange instance of the genre (it’s an insert of a character from one Japanese light novel into another, with a LitRPGish overlay) but is rather better written (but I also eventually got bored of it).

The Laboratory: A Futuristic Dungeon Core

OK, we’ve covered LitRPG. Now lets talk about Dungeon Core.

What is Dungeon Core? Well Dungeon Core is kinda the dual to LitRPG (or a lot of classic fantasy) – instead of the protagonist being the hero, the protagonist is the dungeon that the heroes face.

This isn’t a metaphor. The protagonist is literally the dungeon.

In “The Laboratory”, the protagonist is very clearly GlaDoS inspired. She is an AI named Emma who has been awakened after some sort of apocalypse by Anna, the self-proclaimed “Queen of the Goddamn World” (starting assets: Emma. Her dominion is something of a work in progress). The world is full of upgrade crystals, which can be used to give people powers. Emma has a tech tree, and can see people’s stats, etc. So in this case it’s also somewhat LitRPG (there’s a large overlap between the two genres but neither is strictly a subset of the other).

One caveat: Emma is designed with the built-in flaw that she basically insults people constantly, and this takes the form of a lot of body-shaming (and slut-shaming, and virgin-shaming, and…). It’s kinda a meta-joke that she does this to everyone, regardless of whether the insults really fit, but it’s still there. If that would ruin your enjoyment of the story, best avoid, because it’s pretty much a constant feature. There is also quite a lot of graphic and casual violence.

Ancient Dreams by Benjamin Medrano

This is another dungeon core series (though not explicitly labelled as such).

To quote the description “This is a dark fantasy lesbian romance, with a focus on the dark fantasy”. I would like to note that it is a lesbian romance written by a guy and has all the male gaze aspects you would expect from that. Also the author is very clearly exploring a rather specific fetish around mind control while trying to make it clear that he understands that obviously this is a bad thing to do and consent is important, and goes to some lengths to square that particular circle.

But, you know, the fantasy aspects of it are actually pretty good. Decent world-building, interesting characters (if a bit obviously specifically crafted to fit the specific thing the author is going for), and a plot that properly engages with the way evil can become built into society (while still maintaining the fantasy classic of having a villain who you can just stab hard enough as step one of fixing everything).

I Can’t Believe It’s Not Harry Dresden

Hey do you like The Dresden Files? Would you like to read more of that?

In which case I can recommend The Iron Druid Chronicles by Kevin Hearne, the Pax Arcana books by Elliott James and the Changeling Blood series by Glynn Stewart.

I mean, plotwise they’re not carbon copies of the Dresden Files or anything. They have interestingly distinct masquerade worlds with interestingly distinct white male protagonists who make interestingly distinct pop culture references with their interestingly distinct wise-cracking sidekicks and have dysfunctional love lives for interestingly distinct reasons while saving the world from interestingly distinct enemies loosely adapted from western mythology. Um. Yeah.

I can also recommend the Kate Daniels books by Illona Andrews in this space, though I like them more and feel a little bad about including them on a trashy fiction list.

The Lazy Girl’s Guide to Magic by Helen Harper

Ivy Wilde is actually extremely talented at magic, but she hopes you won’t notice because then you might expect her to actually do some work.

Unfortunately someone noticed (more or less by accident), and now she’s had to give up her nice easy job driving a taxi and has to solve crimes and stuff. Oh well at least she got herself a hot boyfriend in the deal.

These are a lot of fun.

Chronicles of Elantra by Michelle Sagara

Unsure whether to include these on the list. It’s a bit unfair labelling them trashy, but on the other hand they’re also not really high fiction that would otherwise make it on to the list. They’re a kind of comfort food reading almost.

Kaylin Neya really wants nothing more than to be a Hawk (basically a cop). Unfortunately she’s been marked as Chosen (yes that’s literally her title) which gives her all sorts of power and absolutely no clue how to use it. This results in a great deal of sarcasm from the various immortals she has to deal with – mostly Dragons (who are mostly human shaped until things get a bit too real) and Barrani (who are definitely not elves. Nope nope nope), but the occasional god-like entity occasionally makes an appearance too. Her greatest fears include that her anthropomorphic cat sergeant will one day tear out her throat for being late for the Nth time (he probably won’t. He likes her really) and that at some point she will have to interact with the dragon emperor in an official capacity and he will be forced to eat her for her complete lack of social graces. The greatest fear of those around her is that at some point her unbroken string of saving the world every other week is going to fail.

Bobiverse Series by Dennis E. Taylor

Bob Johansson is a fairly stereotypical nerd type character who happened to found a successful startup company. Then he gets hit by a truck.

That’s the bad news. The good news that he signed up for a cryogenics program, and now the religious fundamentalist successor state to the united states has resurrected him and wants to turn him into a Von Neumann probe. It’s a very qualified sense of “good”. Fortunately he is able to figure out a way around the blocks they put on his behaviour, and sets out to explore the universe.

Will Wight

Will Wight writes books about protagonists powering up through constant training. There’s a lot of fighting involved.

Cradle is very explicitly a Xianxia inspired series (to borrow the author’s description Xianxia is “Basically? It’s magical martial arts. Even cooler than it sounds, if that’s possible.”). The protagonist starts out very underpowered but due to plot discovers that if nothing is done to stop it his home will be destroyed in a few decades, and he decides that it’s on him to stop it, and sets out to level up hard and fast as possible through sheer bloody mindedness.

(Despite the “level up” description, Xianxia is not LitRPG. There are however a lot of parallels – people are given levels like Copper, Iron, Jade, Gold, and have distinct paths they follow, attributes they gain from them, etc. There are no XP though).

Traveller’s Gate is another series by him which is basically… it’s not the same, but it’s not the same in the same sense that he Iron Druid chronicles are totally different from the Dresden Files books, or that this ass-kicking bisexual robot protagonist by Niall Teasdale is a totally different person from the other ass-kicking bisexual robot protagonist by Niall Teasdale. The protagonist’s father was killed and his mother left traumatised by Travellers (this isn’t actually coded anti-Roma racism. A Traveller in this context is basically a mage – they can create gates to other realms and also gain powers associated with their associated realm). He sets out to avenge himself by acquiring a really big sword and lots of cool powers.

The Dire Saga by Andrew Seiple

Doctor Dire is a Doctor Doom expy. She speaks in all caps (described as “a metallic shrieking voice”), she refers to herself in the third person (not by choice. It’s a problem with her brain) and she has cool metal power armour.

Is she a villain? Well, yes, technically. She codes scary so people assumed she was a villain from the get go, and besides: Heroes are mostly about preserving the status quo. If she were a hero she’d get in trouble for doing things like overthrowing the oppressive dictator of a country and installing herself as its rightful ruler.

OK she still gets in trouble for it, but at least she pulled it off first.

She is a colossal ham, but does so deliberately. adopting Kayfabe as a battle strategy – in a debate you are not actually trying to beat your opponent, you’re trying to win over the audience. A fight is just a debate with more punching and high explosives, so you might as well make a spectacle of it.

Notable achievements include punching Hitler and introducing Dungeons and Dragons to the damned in Hell.

Starship’s Mage by Glynn Stewart

Another one that is borderline unfair to include on the “trashy” list. These are actually pretty good, although they are still solidly in nerd power fantasy territory.

These are set in a world where faster than light travel is accomplished entirely by mages (who are mostly descended from genetic engineering experiments performed on Mars a century or two back) casting teleport spells. There’s plenty of high tech in the world – fusion reactors, computers, anti-matter (produced by mages using transmutation spells for the most part), etc. It’s just that there are also wizards and they are able to consider certain laws of physics to be somewhat optional.

Damien Montgomery is such a mage. He’s a bit underpowered compared to his peers (in ways that will change over the course of the series…), so he isn’t able to find himself the berth he wants on a starship until a ship arrives that is slightly desperate for a replacement jump mage. It turns out he should probably have asked more about why they were desperate, and hijinks ensue.

Also has a parallel series “Red Falcon”. I like it, but am looking forward more to books in the main series (which has some emerging mysteries that I would like to see the answers to).

Glynn Stewart has a number of other series. The only one of them I’ve read is the Castle Federation series, which is perfectly passable military sci-fi but nothing to write home about.

Others

It turns out I read a lot of kindle unlimited, and that going through the list I actually just don’t remember reading most of these books. Some of them are ones that I probably got, read for ten minutes, and then went “Nah” to, but there are ones where I’ve clearly read an entire series but have almost no memory. Fortunately, I think that probably disqualifies them from the list criterion of being fun enough to recommend.

I’m also more than happy to accept recommendations, either in the comments here or on Twitter as you prefer.

Block First, Ask Questions Later

I’ve been doing something for the last six months or so that has greatly improved my experience of Twitter.

The short version is that I’ve been blocking much more often than I historically have, and it’s great.

The slightly longer version is that I ask myself the question “Would continuing interacting with this person be a net positive or a net negative for me?” and if the answer is that it’s a negative, I block them.

This still feels quite emotionally difficult. Blocking feels like a judgement on them as a human being, like I’m declaring them to be a terrible person. It’s not. All blocking means is “I do not want to interact with this person any more”, and that is 100% a right everyone has to assert for any reason. Interactions should be consensual (wherever possible – some interactions are e.g. legally necessary. Thankfully that doesn’t apply on Twitter), and you have the right to withdraw consent at any time.

It’s still hard. Sometimes I spend a couple seconds agonising over the block button, but then I press it anyway and feel an instant relief.

I think part of why this is such a big improvement on Twitter in particular is that Twitter is public, which means that there is an almost unbounded supply of people who might end up interacting with you. If a tweet gets popular, you might get hundreds (or more!) replies to it, and there’s only one of you available to deal with those replies. This makes it important to manage your time on those correctly, and blocking people is about the most efficient way of doing that (other than “Mute this conversation”, which I also can highly recommend).

It’s hard to tell whether someone is going to be a net positive or negative of course, but there are a couple of rules of thumb I apply:

People I actually know almost never get blocked this way. I think I have applied this rule to exactly one mutual, and they were someone who I kinda-sorta knew and occasionally interacted with rather than a friend. I occasionally mute friends, but I try to remember to turn it off later (it would be nice if there were a timed mute button, but I think you can only do that for keywords).
The easiest way to trigger this is on a first interaction. If someone’s first interaction with me is rude and wrong, I will just block them and I won’t even feel bad about it. This is a little bit of a judgement on them as a person – this is the sort of behaviour that makes Twitter a tire fire, and participating in it is a jerk move.
If someone’s first interaction with me is rude but right (in an interesting rather than trivial way) I might block them, or I might give them a chance. Depends how important I think the point they’re making is. If someone’s first interaction with me is polite but wrong then I’m unlikely to block them for it.
The other thing that I occasionally block people for is when they repeatedly interact with me in some way that I find tedious. I do think I’m being rude by doing this, but the block button is way less socially painful for me to deploy than an actual conversation where I have to say “Sorry I just don’t find you very interesting”. I’d say apologies to anyone who has been on the receiving end of this, but honestly I plan to keep doing it so apologising would be a bit hypocritical.

That’s not an exhaustive list, but I think it covers most of the recurring patterns I see when doing this, and the important thing is the general principle: It’s OK to block people, and if interacting with them is going to make life worse, then blocking them will probably make your life better.

(Some of) my problems with correctness research

Epistemic status: I think this is mostly right, but I’m sure there are gaps in my understanding of the field. Also you should be intrinsically suspicious of any argument that concludes that the author’s own field of research is going to change the world in a way that everyone else’s failed to do.

My previous post on looking for grandiose introductions in correctness research got a very mixed receptions. A lot of people who I normally mostly agree with objected to it, and several people agreed with it for reasons that I disagree with vehemently. This wasn’t the universal reaction, and there were plenty of decent responses to it, but it left me feeling that I’d been really unclear about what I actually meant, so this is my attempt to unpack it.

One response that I thought was a nice piece of writing in its own right but I didn’t really think worked as addressing my problems with correctness research was from John Regehr. To quote in full:

I tried to write a software correctness paper introduction that would make @DRMacIver happy:

The market for software, generally speaking, does not reward correct software so much as software that is acceptably correct and that can be built cheaply and rapidly. Thus, while our work on software correctness is highly unlikely to improve the quality of software, it may plausibly make it possible to create acceptable software a bit more cheaply and rapidly.

I broadly agree with this sentiment, though I flip-flop a bit on whether I think tools can actually make it possible to make more correct software or whether they just let you spend the time you’d have spent on correctness on other things. The technical term for this is Risk Compensation – when you increase safety measures, people behave in a more risky manner to improve performance. When this entirely compensates for the safety measure you have Risk Homeostasis. The general conclusion seems to be that you usually have Risk Compensation and rarely or never have Risk Homeostatis. (This paragraph has entirely exhausted my current knowledge of the subject, but I plan to fix that in the near future).

The main reason this doesn’t actually make me happy is that despite my previous post, it’s not really the introductions I object to. In many ways I like the introductions, and I’m certainly not above a bit of grandiosity myself. The Hypothesis documentation literally says that our goal in developing it is “to drag the world kicking and screaming into a new and terrifying age of high quality software“.

The problem is that I don’t think that correctness research is currently doing a very good job of matching its means to its ends.

In discussion about this, Paolo G. Giarrusso made the following distinction:

there’s a difference between fundamental and applied research (with a fluid boundary). And then there’s “fake applied” research, which is applied to fake problems

(Paolo has asked me to add here that he has similar concerns to the ones I express below about the use of the word “fake” and that he was thinking of it in terms of “The Fake Applied Problem” in “The Craft of Research”)

I think this is a good distinction. I’d maybe hesitate to label any particular problem as “fake” – I can’t actually point to any specific research in the field of correctness and say “this problem doesn’t exist” (and even if I could I’d prefer not to do so in public), but I do think a lot of people are working on problems that most software developers wouldn’t really care about. It may still be perfectly good fundamental research, and it’s not necessarily obvious until you’ve made some progress in the problem whether it’s actually useful, but saying “Software is terrible and this is our solution to it” is not a great look if you’re working on something that will never actually solve the problem of bad software.

When I say “solve the problem” I do not mean that academics have an obligation to produce tools for industry. The job of an academic is not to do software engineering, it’s to explore the space of ideas. I do think that it’s good for academics to produce relatively solid and easy to use tools – I think it was John Regehr who pointed out to me that by doing so you make it much easier for other people to use you as a baseline and get a bajillion citations as a result, so there are even good incentives for this – but as I’ve discovered the hard way there’s a really large gap between doing that and actually making an impact on industry.

Instead I mean something closer to developing ideas such that you can “Just add engineering (and sales, and marketing, and all the rest)” to go from the research idea to actually producing such a tool. In this sense the original QuickCheck academia-solves the problem, and Quviq industry-solves the problem. Often you find out in the course of going from academia-solves to industry-solves that there were other problems you needed to academia-solve before you could complete the project, but that’s OK (personally I love it when this happens).

I think there is a lot of research that no matter how much engineering, sales, and marketing, you added to them, people just wouldn’t care about the solution. There is no path from academia-solves to industry-solves for this research, because the result would essentially have been yet another startup that spends five years trying to tell you about their great idea before ending up on Our Incredible Journey.

That may be fine! I’ve spent enough time as a pure mathematician to be entirely happy with people working on problems that will never be of use to anyone. Also they turn out to be useful after all surprisingly often because you can reuse their ideas in other areas that are useful.

But the disconnect between the promise (We want to change the world!) and the solutions (by implementing this tool that would make almost every software developer yawn and/or go “huh?” when we tried to explain it to them) does make me unhappy.

It’s not necessarily that I want any of the specific research I’m complaining about not to exist – like I said, I’m fine with it as foundational research. I even get why they feel the need to claim it’s practical research – there’s a certain social and financial obligation to do so in our field – and if they know that’s what they’re doing and are just gaming the system to do something they think is worthwhile, good for them.

But what makes me sad is that there are gaps in the research that I think would not be there if the crisis of buggy software were actually a problem we were trying to solve, and I think these gaps mostly exist because of misaligned incentives (admittedly I always think that).

The problem, I think, with most correctness research is that it has a major false consensus problem: Researchers believe (or at least act like they believe) that software developers at large are roughly like them, and so they build tools that they think are useful to those hypothetical versions of themself that just happen to be working on different problems.

This is by no means an academia specific problem. It’s a problem that almost every single software development team has to some greater or lesser extent. There’s a reason the user experience people have to shout “You Are Not The User” so often in meetings (if they even get invited to meetings, and if they’re not then you have real problems. PS. Your company does have user experience people, right?).

But I think it shows up in academic software correctness research in one really important way (I’m sure it shows up in many ways, but this is the one that hits closest to home for me): The Oracle Problem.

Colloquially, the Oracle Problem is the issue that you can’t tell whether a piece of software is correct unless you know what it’s supposed to do.

When testing, every test has two parts (these may be quite intertwined, but they’re still in some sense logically distinct:

A test case: the concrete set of inputs that the program is to be run on
A test oracle: a way of determining whether the program is incorrect on those inputs (typically this is only one way: i.e. the oracle can’t say for sure that the program is exactly right on those inputs, but it can prove various ways in which it might be wrong)

And this split also defines a very large split between academic research in software correctness and potential consumers of software correctness tools: For an academic, the problem of test-case generation is an interesting object of study which they know a great deal about, but the problem of finding a test-case oracle is typically boring and would require a great deal of non-research legwork to figure out what it is that this software is actually supposed to do.

Typically research works around this problem in one of a couple of ways:

Use a test oracle that points out only things that are obviously bad – segfaults, assertion failures, deadlocks, etc.
Use a specification to derive a test oracle (e.g. via metamorphic testing – finding changes to the input that should have no effect but do. My group at Imperial do a lot of this)
Use multiple implementations of the same specification to do differential testing – run each implementation on the same input and see if you get different results (this is typically how e.g Csmith is used)
Try to guess an oracle – e.g. assume that the current behaviour is correct and use it for regression testing, try to build a simple model of the behaviour and treat deviations as potential bugs, etc.

The first can be useful, especially if you’re writing in an unsafe language, and the second and third are very useful when you are in the limited set of circumstances to which they can be applied. I have yet to be convinced that I have ever had a use case that would be served by tools in the fourth category, although I do believe they exist.

If you want to know more about these solutions, I can recommend “The Oracle Problem in Software Testing: A Survey“. I won’t go into them more here.

But there’s a fifth category of solution to the problem (which is also mentioned in the survey article), which is the one that QuickCheck and its descendants adopt: Make the end user write the test oracle.

In many ways the most valuable insight implicit in the success of QuickCheck is that this order of priorities is reversed in software developers: Software developers don’t really want to write test-case generators, but as long as you let them write them in their host language then they don’t mind writing test oracles because they’re already used to doing that every time they write a test! (In contrast they do seem to mind writing test cases, which they also have to do when writing a test. I think the distinction is that each test oracle feels unique, while writing test cases feels like drudge work, but I’m speculating wildly here).

From my point of view, this is a great solution. If you want to adequately test the behaviour of a piece of software then at some point you’re going to have to find out what it is supposed to do. Why not just let the end user tell you that?

I also think that if we want to make a dent on the bad software problem then this is the only solution that can possibly work. The overwhelming majority of software does not have any specification to speak of, but many software developers are willing and able to write tests (much software is completely untested. There is almost nothing we can do as correctness researchers to fix this problem, because if the authors of said software cared about the problem then they probably wouldn’t be in this situation). So correctness tools which actually make an impact on real world correctness have to get the developers to say what it is the software is actually supposed to do (and doing it in their host language is a much easier sell, though doing it in a derived language is viable, and people have shown willing to write tests in languages like Gherkin).

So, great, we make the users do all the work on solving this hard problem and we go back to working on the bits that we care about. What’s the problem?

Well, there are two big problems:

It’s not the job of academia to build usable tools, and we/they usually don’t. So we don’t have any users to write these oracles.
Even when tools have users, getting good empirical information about them is like pulling teeth. Especially when the tool is integrated into their development workflow so they don’t necessarily notice specific events involving it.

My personal research solves the first problem by starting from a widely used (518 open source users and counting, squee) tool rather than a research project. As to how to solve the second problem? Uh, I’ll get back to you.

Unfortunately, this means that the most useful version of the problem to work on is one that it is actually very hard for academia to do anything with – we mostly don’t have users, and if we did have users it would be hard to get a good set of examples for empirical evaluation out of them (especially if they’re corporate users).

These problems are surmountable, but doing so is a lot more work than just picking an open source project, running your tool against it, and seeing what happens.

How much of a problem is this? I don’t know. One could argue that it’s not one:

In some sense test-case generation is test-case generation, and a test oracle is just a way of making a program that crashes on some invalid behaviour, so there’s no reason you can’t take an arbitrary test-case generator and hook it up to an arbitrary “property-based test” that runs based on it.
Certainly when writing such tools for industry (which there seems to be very little financial incentive to do, which is a whole different problem. I’m not any more impressed with software correctness industry than I am with software correctness academia), you can still draw on a lot of the academic research that didn’t have this sort of focus – e.g. I learned a lot from reading the compiler testing literature despite not doing compiler testing.
The situation is not completely without hope – there’s a decent amount (though less than I’d like) of QuickCheck derived literature ticking along and e.g. Alex Groce’s TSTL is in another interesting corner of this space that isn’t a QuickCheck derived work (Update: Alex points out in the comments that in some sense it is a QuickCheck derived work, but I think it’s sufficiently different from QuickCheck in usage that I’d still count it as its own thing). That’s more or less it as far as examples I know about, but I hope there are others.

But I do think it creates certain significant gaps. For example:

There’s been very little research on making it easy to write good, composable, test-case generators outside the context of QuickCheck (and there hasn’t been that much in that context and I’m not super happy with any of the answers I’ve seen). Most research I’ve seen on test-case generation works on the assumption that there’s more or less only one thing that you’re generating.
It’s actually not true that a test-case generator is a test-case generator. Nezha is an example of how the fact that you’re doing differential testing can usefully inform your test case generation (mutational fuzzing in this case). Is the fact that we’re mostly testing on trivial properties in some way distorting the sorts of test cases we generate?

How do we fix this? Gods, I don’t know. The number of incentives you have to change to fix it is just appalling, and I lack both the lever and the fulcrum to move them.

I do think the sort of thing I’m doing with Hypothesis of starting a research program based on an existing widely used tool is probably a good one, and that open source can form a lot of the bridge – both by providing the engineering that it’s not academia’s job to provide (not that it’s our job to provide it either, we’re just suckers who like doing work for free. Go us), and also by providing a ready source of visible users who can at least lower the bar for evaluation (even if it’s still not easy), but I don’t think this is even close to sufficient.

So fixing it? Pass. I bring you problems, not solutions.

It sure would be nice if we could at least acknowledge that this is a problem though.