Random (short) musings

On Friday, the Perserverence rover landed on mars. Now that it's landed, it needs new software for the next phase of its mission:

You think patching is hard? NASA is about to do it on Perseverance on Mars.

— Don Edwards (@DMEdwards) February 19, 2021

But if you think that's hard, wait until you hear what happened to the Pathfinder rover in 1997. Every so often, it randomly rebooted itself and lost some data. The engineers on the team managed to remotely diagnose and fix the problem. You can read about their process, what the problem was, and how they fixed it here.

If you're keen for even more SPACE COMPUTERS stories, there's a good one here about diagnosing and fixing a problem in voyager 2, at the edge of the solar system, in 2010. That's twenty-nine years after it was originally intended to be shut down. That article has a bunch of updates at the top of the page, so I found it easiest to read from the bottom-up. So far as I can tell, the problem they fixed wasn't even a "software bug" per se… It looks like an important bit got flipped by a cosmic ray.

The radio this morning said that the PM is expected to give an important speech today about a new five-year "extremism strategy". The home secretary said that legislation was only a small part of the strategy, and that it was about all forms of extremism, not just "Muslim extremism". As I write this, the speech hasn't been given, and I don't know any more details. What I'm hoping is that the PM will talk about racism in the same breath as he talks about extremism.

It seems to me that a great way of encouraging young folks to latch on to a handy extremist ideology is to "other" them from the society they're living in. You can try to prevent this from happening by removing the local sources of extremist ideology, and to some extent that seems like it might work. But we still have the internet, and people can still make stuff up themselves. If a young person feels excluded from British society they might find themselves motivated enough to do just that. The other obvious thing we can do is try to not exclude people from our society. That way they might be less motivated to seek out (or invent) extremist ideologies in the first place.

If the PM wants to support a positive integrated multi-racial narrative for the UK, and if he does that in part by cracking down on hate speech; then I think it's vital that he crack down on hate speech by the majority at least as much as he cracks down on hate speech by minorities. This may well mean engaging in some way with the popular press.

Imagine how easy it would be as a Christian in middle-England, to hear stories about anti-Christian persecution in Afghanistan, and start to fear your new Muslim neighbours. Or as an atheist in Cosmopolitan London, to read about anti-atheist sentiment in the US bible belt and take it out on the Christian middle-Englander. Or as a Muslim in Malaysia, knowing about US/Europe-led Christian/capitalist global politics, to worry about the thin end of the wedge in your own country.

I think it's probably tough enough to actively realize that you're in the majority, even when you don't have access to up-to-the-minute news stories about all the places where you wouldn't be. So good on this person, for realizing and expressing just that.

When talking about testing, formal methods people often make an argument that goes something like this:

There is an infinite space of possible inputs to most deterministic programs, and hence an infinite number of behaviours that these programs might exhibit. There is a smaller space of the behaviours we want the program to exhibit. A single test allows us to pick one set of inputs, and observe a single point in the space of behaviours a program actually exhibits. So unittesting can be used to observe a scattering of points in the space of behaviours a program does exhibit, and check that each of these points falls within the space of behaviours we want.

If a test fails, it means we have found a point in the input-space which results in behaviour that falls outside the specification space. If all our tests pass, it means we haven't yet found such a point. But it can't mean that no such points exist, since we can't have explored the whole (infinite) space yet.

In contrast, a formal proof explicitly proves that all the inputs of a program do result in behaviours that fall within the space of behaviours we want. If we fail to find a proof that means nothing, but if we find a proof, then we know for sure that the program does exactly what we said we wanted it to do.

While testing is nice, things will only ever be properly reliable if you listen to us and prove things. So nyah.

I wonder if this view misses an important point about good tests. Good tests are supposed to be corner cases. For example, there's this idea that if I test my simple natural-number function with 0, 1, and maybe some largeish number like 387 (and MAX_NAT if you have such a thing), then that ought to catch most genuine errors¹.

I wonder if this idea of corner-case testing corresponds to base-cases in inductions in formal proofs of the same programs? Perhaps, in the case of the natural-number function, 0 is the base case, and the case 1 presumably corresponds to the inductive step.

I know that there are many good lines of research on things like concolic testing, and I think I've heard to theorems which show that all possible race conditions in certain classes of programs can be discovered with only a small number of threads (of the order of 2 or 3). I know that model checking tools and things like FDR do all sorts of clever things to reduce the size of the state space they have to explore. But I'm not sure if I've seen the possible link between corner cases and induction explicitly made anywhere.

Obviously testing a natural-number function with just 0 and 1 is likely to be a bit optimistic for all but the simplest functions – but this is my point. A function which (for example) treats even and odd numbers differently will likely have two base cases, not just one. Most of the functions we write in practice are quite complicated, and have many corner cases. If those corner-cases are already explicitly enumerated in the form of unittests, and if they correspond to the base cases and inductive steps, then perhaps they can be used as hints by some automatic tool which is attempting to discover and verify that induction (or those intertwined inductions). Or perhaps such a tool could provide useful feedback to a tester, if it discovers that a base case is missing?

If there is a strong connection between "good tests" (which cover all the corner cases) and inductive proofs of programs, and if the tests run much faster than the verification tool, then perhaps we can exploit the connection to run the fast tests on every commit, and the slow verification tool only nightly.

Perhaps this is all obviously flawed, or else already being done somewhere. Tweet me a link if you know where.