Can you name a documented nontrivial program with >1000 lines of code that ran correctly on the first try? What data exists on long computer programs that were not tested early on in their development?

Well, the software that runs the critical systems on the Space Shuttle is a common example. Yes, the components that make up the software probably underwent unit testing prior to launch, but testing (and debugging) made up only a very small fraction of the cost of assuring the software would not fail.

Correctness proofs and other formal techniques are used to verify all modern mass-market high-performance microprocessor designs, a la Intel and AMD. The techniques used to verify the designs above the level of abstraction of the logic gate are largely tranferable to software.

A lot of military systems use formal techniques to verify the software. Warplanes for example have used "fly-by-wire" for decades: in a "fly-by-wire" plane, loss of function of the fly-by-wire system causes the plane to drop out of the sky or immediately to go into a spin or something dire like that. I believe the fly-by-wire system of modern warplanes entails significant amounts of software (in addition to digital electronics), but I am not completely sure.

Just because most software-development efforts do not need and do not want to pay for formal methods does not mean that formal methods do not exist or that they have not been successfully used in ambitious efforts.

it seems to me that proving honesty would be considerably easier. If you can prove that an AI is honest and you've got a strong box for it, then you can modify its source code until it says the kind of thing you want in your conversations with it

These notions of honesty and conversation seem kind of anthropormophic. I agree that we want a transparent AI, something that we know what it's doing and why, but the means by which such transparency could be achieved would probably not be very similar to what a human does when she's trying to tell you the truth. I would actually guess that AI transparency would be much simpler than human honesty in some relevant sense. When you ask a human, "Well, why did you do this-and-such?" she'll use introspection to magically come up with a loose tangle of thoughts which sort-of kind-of resemble a high-level explanation which is probably wrong, and then try to tell you about the experience using mere words which you probably won't understand. Whereas one might imagine asking a cleanly-designed AI the same question, and getting back a detailed printout of what actually happened.

Traceback (most recent call last):
File "si-ai.py", line 5945434, in <module>
if Neuron_0X$a8f3==True: a8prop(0X$a8f3,234):
File "si-ai.py", line 5945989, in a8prop ...

And if there really is a race going on between those who are concerned with AI safety and those who aren't, it likely makes sense for those who are concerned with safety to do a certain amount of corner-cutting.

This is a good argument against wasting a bunch of time on elaborate physical safeguards.

Do you disagree with her?

Nope. Specifying goal systems is FAI work, not AI work.

So then simpler utility functions will be easier to code and easier to prove correct.

Relative to ancient Greece, building a .45 caliber semiautomatic pistol isn't much harder than building a .22 caliber semiautomatic pistol. You might think the weaker weapon would be less work, but most of the problem doesn't scale all that much with the weapon strength.