……是的，一些重要的程序可以被可靠地验证，各种局部属性可以使这更容易，这很有用，但由于软件的发展速度远超有效形式验证的规模，而且我们对软件验证复杂性的了解更多，因此今天“普通”软件的端到端验证比50年前更遥不可及。这就是为什么软件保障研究的重心正在向非可靠方法转移。我认为，关注可靠性并不会帮助提高软件的正确性，反而会分散对更有成效的技术的注意力。‘我们可以验证很多’和‘我们能验证的只是九牛一毛’这两者同时成立，但这种差距常常在形式方法的讨论中被忽视。
源讨论关于Rust、可变别名和形式验证的一些笔记原帖 145 条评论 · 导入时统计把你的经验，加入这段讨论。
我认为展望一下验证小型Rust库是否正确使用'unsafe'是合理的。仅这一点就会非常有帮助。
完整原文附言 我认为，关注正确性并不有助于推动更正确的软件，反而会分散对那些在实践中已被证明更有效（并得到理论支持）的技术的注意力——有时甚至会让以前认为正确性是唯一途径的人感到惊讶，例如：http://users.csc.calpoly.edu/~gfisher/classes/509/handouts/h... 。这种情况反复出现：在正确性方法有重要改进的同时，不正确的方法在实践中正取得更大的进展。这里只是一个非常近期的例子（甚至可能不是不正确方法的最前沿）：https://antithesis.com 当然，这是一个非常复杂的话题，因为在某些特定情况下，正确性技术更强大且实用。
完整原文您好，Presler先生， 我不知道您是否意识到，过去至少6年里，您在Hacker News上无数次重复了同样的论点，而在这期间您却从未在收到许多评论后增加任何细微差别。您并非完全错误，但离完全正确也差得很远，因为世界上有一半对这个话题感兴趣的人已经多次向您展示了这一点，您在数百次提出这个论点时都有机会看到。 而且，除了您不断重复的论点之外，令人着迷的是，您在这么长时间内完全没有改变自己的立场，这表明您从未从这些与他人的讨论中学习到任何东西。 这真的听起来像是病态的固执己见，这意味着与您交流的人浪费了他们的时间，而这正是您应该认真思考的事情。 此致
完整原文尊重不同观点，分享具体经验。
登录后即可发帖、评论、转发和引用。