I am fairly confident that we can tweak any correct program into a form which allows a mathematical proof that the program behavior meets some formal specification of "Friendly".

I am less confident that we will be able to convince ourselves that the formal specification of "Friendly" that we employ is really something that we want.

We can prove there are no bugs in the program, but we can't prove there are no bugs in the program specification. Because the "proof" of the specification requires that all of the stakeholders actually look at that specification of "Friendly", think about that specification, and then bet their lives on the assertion that this is indeed what they want.

What is a "stakeholder", you ask? Well, what I really mean is pitchfork-holder. Stakes are from a different movie.