Notes

Good discussion with Ross today, resulting in one nice, concrete idea.

Consider the problem of suggesting policy improvements to the government. In particular, let’s imagine someone has a specific, detailed policy change related to health care, financial regulation, etc. Presumably, the people who know the most about these industries are (or were) in the industries themselves, so you could argue that they can’t be trusted to propose ideas that aren’t just self-serving. Maybe it’s possible for someone to build a reputation of trustworthiness, but that’s hard and would ideally be unrelated to the actual ideas proposed. Instead of relying on reputation, we’ll remove the issue entirely by making the suggestion box anonymous.

Now we have an anonymous suggestion box on a website. People go to it and propose ideas. There are a few good ideas, and a vast amount of bad, malicious, and nonsense ideas (including spam). Eliminating the spam is easy (I have a single, completely public email address and get roughly one spam message per day, from which I conclude that the spam issue is solved). In order to eliminate the bad or malicious ideas, we need to be able to judge their correctness in a logical manner. For this, we rely on distributed intelligence: other people are allowed to judge whether each idea is good or bad. To get loaded words out of the picture, let’s replace “good” and “bad” with the words “true” and “false”. “Ideas” become propositions of the form “Implementing this idea would be good” (yes, “good” is still there, but keep reading).

Let’s assuming voting isn’t a completely reliable system for determine the truth or falsity of ideas (otherwise, we’re done). Therefore, some true propositions will get a lot of false votes, and vice versa. To solve this, we allow people to propose arguments for or against each proposition. These have the form of some statement, like “That proposition is false because the author is a moron”, together with a more details argument for why the statement is true. Now we let people vote on two more things:

1. Whether the truth of the statement would imply that the original proposition is true or false.
2. Whether the argument for the truth of the statement itself is sound.

If we get enough votes in favor of both (1) and (2), we conclude that the original idea is true (or false), and discount the votes for or against the original idea.

This is the key part, so I’ll restate it. If we have propositions $A$, $B$, and $B\Rightarrow A$, then enough votes for both $B$ and $B\Rightarrow A$ override any votes against $A$. You can’t kill a good idea unless you can the arguments for it as well.

Now we have to get recursive. What if $B$ gets a lot of votes, but is actually wrong? Then you let people propose arguments for the falsity of $B$, and so on. What if there are two competing arguments which appear to contradict? Then you let people propose arguments about why there isn’t a contradiction? There are a lot of logical issues to deal with, but people can post arbitrary arguments written in normal human languages and we have the full power of human intelligence to judge them, so we’re not limited by artificial logical restrictions. This isn’t a formal proof system.

Unfortunately, we are limited by what happens along the full recursive tree. If people lie about the propositions all the way down, and manage to flood away all the counter arguments, the system will fail. However, this is basically a problem of spam, and can be solved in the usual way. If you detect that someone is consistently voting opposite the correct answer, you flag them as malicious and discount their votes. This rule is circular, but that’s what probabilistic analysis is for: we take all the data and compute the most likely assignment of truth values to propositions and spam flags to people. There’s some threshold of validity that you need to achieve in order to such a solver to converge to the correct answer, but that level of trust is often quite low due to network effects and self-reinforcement. In other words, contradictions don’t fit together.

Since this is a website, we have to identify whether the “users” are actually people. We could do this conventionally with a system like ReCAPTCHA, but since we’re in recursive mode it’s much cooler to instead ask users to judge the correctness of randomly selected propositions. If you want to vote on whether a proposition is true or false, or propose a new proposition, you need to spent a little time judging the ideas of others. If someone comes up with a way to trick this system by writing a program that can judge the truth or falsity or arbitrary English propositions, this discussion may be obsolete (thanks to Ross for this particular bit of reasoning).

Other issues probably abound, but they can be fixed by allowing people to suggest improvements to the system. If deemed reasonable, these ideas can be implemented and tested in parallel with the existing system, resulting in a potentially large number of competing systems for determining truth values from the same data set. The data set itself could probably be made freely available (under a suitable license), so that others could build competing systems.

I don’t think this system would be all that difficult to implement. Thanks to the previous paragraph, if it reached a sufficient level of quality it would start to improve itself. Maybe that would even get scary.

Of course, if we apply this to a realm like politics, the truth or falsity of various statements will be very controversial, and different people will have legitimately different opinions. This can be solved by adding side conditions to the statements, like “If you believe in flat tax systems, we should do this” or “If you believe that health care is a basic human right, we should do that.” More importantly, however, there is a vast range of ideas that any rational person should agree to. Statements like “the proposed health care bills do not include death panels”, and “given an otherwise equivalent choice between taxing a public good and a public evil, we should tax the latter.” I think it’s fair to say that the U.S. would be better off if we could agree on the statements that don’t need side conditions.

Note: I’ve done zero checking to see if this has been proposed or implemented before (this discussion happen just now), so I’m curious if anyone knows related references or links.

Another note: presumably this would be set up as a nonprofit supported by donations of some kind. If this system actually existed, I would probably be willing to donate at least $1000.

Here’s a summary of the differences between typed functional languages and unsafe languages:

• Difficulty of easy things: Haskell ~ C
• Difficulty of hard things: Haskell < C
• Difficulty of impossible things: Haskell >> C

Kudos to anyone who knows what this means.

Imagine a computer stored in a box with a single small hole connecting it to the outside world. We are able to run programs inside the box and receive the results through the hole. In fact, in a sense results are all we can see; if the program makes efficient use of the hardware inside, the size of the hole will prevent us from knowing exactly what went on inside the box (unless we simulate the workings of the box somewhere else, but then the box is useless).

The human brain is a good example. To an outside observer, the hole is speech; other people can’t know what you’re thinking any faster than you can say it. However, speech is also the hole to ourselves. As I write these words, I am only fully aware of them as they appear on the screen in front of me. Until then, I do not consciously know what they are. I can choose to become conscious of them if I say the words to myself internally, but I must slow down in order to do this. The reason is that I am capable of being fully conscious of only one thing at a time, and it is more efficient to be conscious of the words visually on the screen rather than as I “think” of them.

Thus, we have a trade-off between consciousness and efficiency. In order to be fully aware of our thoughts, we must slow them down until they fit through the hole of consciousness. Conscious thought is necessary in order to correct mistakes in our thinking, remember our conclusions, and communicate with others. However, since our brains are internally structured as a massive parallel computer, the only way to use our brains efficiently is to not be aware of what we’re thinking.

This trade-off applies to thoughts of all kinds, and most areas of human endeavor require carefully switching between the different modes. For example, working out a mathematical proof is often said to require intuitive “leaps” of thought. The reasons these appear as leaps is not because they are actually sudden; our brain does not sit around doing nothing and then suddenly have the idea. Rather, our unconscious mind is considering various different avenues of thought in parallel. If an avenue appears fruitful, the unconscious part will make it available to the conscious part, and it seems to “pop into our minds”. Similarly, it is very difficult to consciously try to remember a particular fact. If you let your mind wander, the unconscious part is better able to search around for what we need in a massively parallel fashion, providing us with the answer asynchronously.

Movement is the same. When you dodge a ball thrown at you, your unconscious sees the ball and moves out of the way before there is time to articulate what is happening. Soon afterwards, your brain retroactively explains what happened: “If anyone asks, say we saw the ball coming towards us and dodged.” One of my hobbies is swiveling to fit through doors as they close without touching them. The last time I did this, I had a vague memory of my vision dimming during this motion, almost as if I was passing out. I think this effect was my consciousness temporarily shutting down to avoid interfering with the reflexive motion.

The same trade-off applies to computers and algorithms. Consider the problem of checking a C++ program for type errors. Current compilers do this by running full template instantiation, which generates code for each instance of the template. In other words, the compiler is “conscious” of the entire process. If we all want is the type errors, it would be much faster to use a specially tailored algorithm that checked for errors only, remembering only enough of the results to speech up the rest of the error checking process. It would be even faster if want to know only whether errors exist, not what they are, since the program could forget line numbers and other details. The cool part is that it is possible to combine the different approaches to get the best of all words: we can running error checking before code generation to reduce the latency of reporting errors back to the user, and we can speed up error checking by first running the stripped down yes/no algorithm and reprocessing any portion that has an error. In a decent programming language, all three variants can be generated from the same source using partial specialization.

This last point is very important, since it means that the trade-off between consciousness and efficiency can often be eliminated; we can start with “fully conscious” code (which remembers everything it does) and apply various “forgetfulness” transformations to shift towards the efficiency side. The different versions can be seamlessly interleaved so that it looks from the outside as if the fully conscious version is operating at the speed of the fastest version; the missing detail is recovered only when we need it. This is similar to human vision; any object we look at appears sharp, so we generally imagine that we see with uniformly high detail. What is actually happening is that almost all of our visual field is blurry, with one high resolution point in the center. We can shift this high resolution point to anywhere we wish, so we get the illusion of uniform sharpness for free.

Taking full advantage of this trade-off to speed up programs will require languages that combine low level and high level features and make it easy for the program to inspect and transform its own code. I’ll write more about this later.

When people discuss the future of computers and software, a common worry is that it will become increasingly difficult to produce correct software due to the ongoing surge in complexity. A common joke is to imagine what cars would be like if they were as buggy as software. I believe these fears are groundless, and that they arise from a misunderstanding of the reason why current software is full of bugs.

Modern software contains bugs because bugs aren’t the problem.

The reason we have bugs in computer software is not because writing bug-free code is impossible. Rather, it is because writing bug-free code is expensive. Eliminating all bugs requires enough extra time and money that it isn’t economically advantageous for the vast majority of applications.

In areas where correctness is more critical, we spend more money and get correctness. Hardware is an excellent example of this: a modern CPU has somewhere around a billion transistors, and is usually bug-free. This is because hardware companies spend vast amounts of money on formal verification methods which rigorously check the correctness of circuit designs. It has to be correct in order to work, so we make it correct. This also applies to software in critical areas: when was the last time you heard about a bug in the software for your car?

For now, most software usually doesn’t need to be correct (witness the explosion of dynamically typed scripting languages). As our dependence on software grows, our demands on its correctness will increase, and software will become correct. To do this, we’ll use a combination of model checking, better languages, formal verification, etc. The ideas required to do this have been around for a long time, are constantly improving, and will improve even faster when we need them more and start devoting real resources to them.

I think this shift will happen soon, but the timing depends primarily on the economics of software, not technical issues. As soon as we’re willing to pay extra to get bug-free software, people will start writing it.

These are very refreshing:

From Hudak et al., “A History of Haskell” [1]:

The fact that Haskell has, thus far, managed the tension between these two strands of development [as a mature language, and as a laboratory in which to explore advanced language design ideas] is perhaps due to an accidental virtue: Haskell has not become too successful. The trouble with runaway success, such as that of Java, is that you get too many users, and the language becomes bogged down in standards, user groups, and legacy issues. In contrast, the Haskell community is small enough, and agile enough, that it usually not only absorbs language changes but positively welcomes them: it’s like throwing red meat to hyenas.

And Alan Perlis [2]:

“I think that it’s extraordinarily important that we in computer science keep fun in computing. When it started out, it was an awful lot of fun. Of course, the paying customers got shafted every now and then, and after a while we began to take their complaints seriously. We began to feel as if we really were responsible for the successful, error-free perfect use of these machines. I don’t think we are. I think we’re responsible for stretching them, setting them off in new directions, and keeping fun in the house. I hope the field of computer science never loses its sense of fun. Above all, I hope we don’t become missionaries. Don’t feel as if you’re Bible salesmen. The world has too many of those already. What you know about computing other people will learn. Don’t feel as if the key to successful computing is only in your hands. What’s in your hands, I think and hope, is intelligence: the ability to see the machine as more than when you were first led up to it, that you can make it more.”

Thanks to Benjamin Russell for pointing these out on the Haskell-cafe list.

[1] Hudak, Paul, Hughes, John, Peyton Jones, Simon, and Wadler, Philip. “A History of Haskell: Being Lazy With Class.” San Diego, California: The Third ACM SIGPLAN History of Programming Languages Conference (HOPL-III) (2007): 12-1 - 12-55, 2007. http://research.microsoft.com/en-us/um/people/simonpj/papers/history-of-haskell/history.pdf

[2] Abelson, Harold and Sussman, Gerald Jay with Sussman, Julie. Structure and Interpretation of Computer Programs, Second Edition. Cambridge, MA: The MIT Press and New York: McGraw-Hill, 1996. http://mitpress.mit.edu/sicp/full-text/book/book-Z-H-3.html