不幸的是，这是极不可能的。

几乎不可能对软件的一般行为做出陈述。这是由于停机问题，它表明无法证明程序是否会因任何给定的输入而停止。从这个结果来看，许多其他事情已被证明是无法证明的。

一段代码是否友好的问题很可能可以归结为停机问题的变体。
在现实世界中运行的人工智能需要“友好”才能有意义，它需要是图灵完备的。来自现实世界的输入无法使用常规或无上下文语言进行可靠解释。

正确性证明适用于具有明确定义的输入和输出的小代码片段。他们表明，在给定正确输入的情况下，算法会产生数学上正确的输出。
但这些都是关于可以用数学严谨定义的情况。

“友善”不是一个严格定义的概念，这已经很难证明任何事情。最重要的是，“友好性”是关于人工智能如何与现实世界相关的，现实世界是一个对人工智能的输入是高度不可预测的环境。

我们所能期望的最好的结果是，人工智能可以被编程为具有保护措施，并且如果可能出现不道德的行为，代码将发出警告标志——人工智能被编程为防御性的。

以下是最近验证自治系统某些属性的一些示例[RoboCheck]。

然而，为了使用形式验证（即“使用数学技术证明正确性”）实现“友好”概念的相同类型的事情，（至少）似乎有必要能够在逻辑范围内表达“友好”形式主义，（即作为模型检查器中可测试的谓词，以便我们可以确定系统永远不会进入不良状态）。

然而，目前尚不清楚“友好”是否比“不伤害人类的愿望”有更具体的定义，因此需要更多低层次的细节。

在这方面可能有用的一般领域的一些先前工作包括：

• Deontic Logic - 义务的逻辑演算。
• Elephant 2000 - John McCarthy 对基于 Promise 的编程语言的描述。