The long-term problem with shutting down progress is that at very best, it just exchanges one form of suicide for another. Death is the default. Without progress, we remain trapped in a sealed box, wallowing in our own filth until something more mundane like nuclear war or pandemic, puts an end to our civilization. Once that happens, it's game over. Even if our species survives the immediate disaster, all the easily accessible fossil fuel deposits are gone. There will be no new Renaissance and Industrial Revolution. We'll be back to banging the rocks together until evolution finds a way to get rid of the overhead of general intelligence, then the sun autoclaves what's left of the biosphere and the unobserved stars spend the next ten trillion years burning down to cinders.

What is being proposed is a small pause in progress in a particularly dangerous field. We can still go on and develop fusion reactors or whatever. We could in principle have a high tech utopian space fairing society, spreading throughout the universe, all designed by human minds with no AI. I mean we probably won't. What is actually being proposed is more like a 20 year pause in AI research to let MIRI solve alignment, and we probably won't get that.

 Even if our species survives the immediate disaster, all the easily accessible fossil fuel deposits are gone. There will be no new Renaissance and Industrial Revolution. We'll be back to banging the rocks together until evolution finds a way to get rid of the overhead of general intelligence,

I think we would probably do something else. Modern crops have been selectively bread and genetically engineered to be much more productive. Thus biofuels would be a better option. Given even a physics textbook, nuclear could be invented quite a bit earlier. (And in a post disaster scenario, their will be a chance to scavenge for fresh nuclear fuel) There is wind power, and hydro power, which become more attractive when you already have sophisticated neodymium magnet generators laying around, or dams already built.

We wouldn't be able to copy the exact route of the industrial revolution. We will find a different route back to high technology. Humans developing tech is like a stream running downhill. Block the easiest route, and the second easiest route is taken. Maybe in economic growth terms, the period takes 500 years, not 200 or something. Maybe its faster because people don't need to invent most of the stuff, just make it.

Pre industrial revolution tech includes stuff like ironwork and pottery, and quite a few other tasks that are complex enough to require intelligence, and useful enough to reward it. 

Unless AI alignment is so easy that humans can figure it out by pure armchair thought, in the absence of actually trying to develop AI.

Fermats last theorem was proved by "pure armchair thought", that doesn't make it "so easy". Suppose AI alignment was a really tricky mathematical problem. Maybe trying to build dumb AI doesn't help, because the behaviour of dumb AI is totally different to the behaviour of superintelligences. And any AI smart enough to give you useful info on superintelligence is smart enough to kill you. 

The default way to think about it is straightforward. Friendliness is a predicate, a quality that an AI has or lacks. A function from a system to a Boolean. (The output could be more complex; it doesn't change the conclusion.) The input is an AI; the output is a Boolean.

The problem – or, let's say, far from the least of the problems – with this formulation is that the function Friendly(AI) is undecidable. Proof: straightforward application of Rice's theorem.

This logic proves too much. It can also applies just as well to the property "adds 2 numbers". This is true. There are some incredibly complicated pieces of code, where it really is impossible to tell if that code adds numbers. 

You can test it on a particular input, but maybe it works on those inputs, but fails on some other input.

def complicated_add(a,b):

    T=get_turing_machine()

    for i in range(a):

         T.step()

    if T.has_halted():

        return a+b-1

    else:

        return a+b

This code is a valid program to add 2 numbers, if and only if T runs forever. 

But we don't want to classify all possible programmes into "adds 2 numbers" or "doesn't add" when building a calculator. We want to find a single program that does add. This is easy. Sometimes we want to verify that a particular algorithm works, this is usually possible, because no one writes software whose behaviour depends on arbitrary turing machines like that.

If you restrict to programs that fit in the universe, rices theorem vanishes. 

Likewise, we don't want to classify all possible programs into friendly or unfriendly. 

On the face of it, this proves too much; Rice's theorem would seem to preclude writing any useful software. The trick is, of course, that we don't start with an arbitrary program and try to prove it does what we want. We develop the software along with the understanding of why it does what we want and not what we don't want, and preferably along with mechanical verification of some relevant properties like absence of various kinds of stray pointer errors. In other words, the design, implementation and verification all develop together.

This also seems to prove too much. Euclid's algorithm was developed and understood as a piece of mathematics long before computers were invented. 

This is not news to anyone who has worked in the software industry. The point is that – if and to the extent it exists at all – AI is software, and is subject to the same rules as any other software project: if you want something that reliably does what you want, design, implementation and verification need to go together. Put that way, it sounds obvious, but it's easy to miss the implications.

You have jumped from formal maths about turing machines that doesn't apply much in reality. And gone straight to advice from a project management book about having your programmers and software testers working in the same office. You seem to imply these are related somehow. The project management bit may or may not be good advice  for the typical software project. It may or may not be good advice for an AI project. It isn't some universal mathematical truth.

"AI is software, and is subject to the same rules as any other software project" AI is technically a software project, but there are some fairly good reasons to expect it to be different from the typical software project. 

It means there is no point trying to create a full-blown AGI by running an opaque optimization process – a single really big neural network, say, or a genetic algorithm with a very large population size – on a lot of hardware, and hoping something amazing jumps out. If I'm right about the actual difficulty of AGI, nothing amazing will happen, and if Eliezer et al are right and brute-force AGI is relatively easy, the result won't have the safety properties you want.

Are you arguing that evolution and gradient descent are so dumb, and AGI is so hard, that no matter how much brute force you throw at the problem, evolution will never create an AGI. (Despite biological evolution producing humans) 

I see no fundamental reason why we couldn't create an AGI like this, and by  reasonably sure it would be friendly due to clever choice of initialization and optimization criteria or transparency tools.

It means there is no point trying to figure out how to verify an arbitrarily complex, opaque blob after the fact. You can't. Verification has to go in tandem with design and implementation.

There is no way to verify every possible program after the fact, if you want a verifier to never make any mistakes in either direction.

If you are ok with your verifier occasionally saying "I don't know", but only on really contrived problems that don't appear in real life, then verification is possible. 

And "big neural nets" aren't arbitrary programs. The net has all sorts of structure to use. 

It means there is no point trying to solve the alignment problem by pure armchair thought. That would be like expecting Babbage and Lovelace to deduce Meltdown/Spectre. It's not going to happen in the absence of actually designing and building systems.

I think these systems were largly designed by humans, and I think those bugs were largely found by humans. In other words, if you got all the chip designers at intel working to produce designs, with no actual silicon being produced, and all the modern security researcher trying to pick holes in the designs, then yes these bugs would have been found entirely by theory. (Of course, no one would pay all these people to do such a useless activity)  

It means suppressing development and shutting down progress is suicide. Death and extinction are the default outcomes. Whatever chance we have of turning our future light cone into a place where joy and wonder exist, depends on making continued progress – quickly, before the window of opportunity slams shut.

Suppose we decided that deepmind wasn't verifying properly. Should we shut them down to let someone who will do the verification try to make AGI.

Suppose every country agreed to total disarmament. The biologists produced one vaccine that stops everything. We build some really good telescopes and several asteroid deflection rockets. Almost all AI research around the globe is shutdown. MIRI is given special permission to carry on, and given the instructions "take your time and do things safe not fast. If it takes a thousand years for you to create aligned AI, that's fine." Do you expect this world to have a better chance at a good long term future than the status quo reality. I do.

'Design, implement and verify' sounds more difficult than just trying to do one of these things in isolation, but that's an illusion. All three activities are necessary parts of the job, each depends on the others, and none will be successfully accomplished in isolation.

MIRI produced a paper on logical induction. This paper proposed an algorithm that was too slow to run in practice. They formally described the algorithm, but didn't program it in any particular language. MIRI managed to mathematically prove some interesting properties of this algorithm. Design and verification without implementation. When producing a really small simple program, I can get it right first try. Design and implementation without verification. 

You also haven't said exactly what each category is. If I write pseudocode. Is that implementation or just design. If I pepper my code with assert statements is that part of verification or just implementation? Does it matter if I haven't run the code yet? Is this supposed to prevent humans writing code entirely by pencil and paper. (Which some humans can do)  

The contention is that we are in a new situation. Writing software is a new type of activity with different constraints than building a bridge; creating a general AI is a new type of activity with different constraints than writing software. In particular, the standard "waterfall doesn't work, agile/iteration is far better" solution to writing software is contended to fail when creating a general AI, specifically because the implement step produces disaster without sufficient design, rather than simply producing failure or waste.

You can argue that we're not in a new situation, but I don't think "it works far better for software ==> we have no choice but to do it for general AI" follows without arguing it.

Of course there are short-term problems with this course of action, such as that it is, if implemented, much more likely to be enforced in democracies than dictatorships, which is very much not an outcome we should want.

There is a reason north Korea isn't in the lead with AI. 

I mean china is a bit more with it, but none of the recent breakthroughs have come from china (that I've seen). 

For whatever reason, dictatorships aren't very good at AI research. Maybe something about censorship, worse education, none of the top researchers wanting to work there. (If your choices were a cushy job at google writing non AI code, or north Koreas internationally condemned AI program, which would you pick? So this will somewhat hold even if all the democracies ban AI research. ) 

I am also not quite clear why north Korea destroying the world would be so much worse than deepmind doing it.