主要观点：

• 收到 Kartik Agaram 的关于“不负责任”服务器的有趣邮件，邮件中提及哥德尔、埃舍尔、巴赫中的一段关于逻辑论证的内容，引出创建指定合同的基础设施的价值及需要诚信或执行机制。
• 介绍了形式系统的相关概念，如可靠（sound）与不可靠（unsound），哥德尔证明了能推出所有真命题的形式系统必定不可靠，存在“无声”（soundless）的漏洞即不可证明/不可判定的句子（独立性）。
• 在应用语义方面，程序员关心正确性，不同编程语言在表达性和可靠性上有差异，目前客户端/服务器间的有趣间隙大多是无声的，“不负责任”的服务器若能提供可用性和协议保证，正确性可在编译时渗透到程序中，虽哥德尔不完全定理保证无声会渗入可靠系统，但可通过信任等方式解决，如 scrapscript 的架构是联邦制，可选择信任的对象，对目前的 REST/gRPC/SOAP 等协议不满，希望程序能在犯错时及时报错。

关键信息：

• 邮件中 Achilles 和 Tortoise 的逻辑论证例子。
• 形式系统可靠与不可靠的定义及相关定理。
• 不同编程语言的特点及在正确性方面的差异。
• “不负责任”服务器与程序正确性的关系及解决办法。

重要细节：

• 提到 Gödel 谋杀数学即证明能推出所有真命题的形式系统不可靠。
• 举例说明 Elm 因其正确性被选择，Vanilla Javascript 有易用性灵活性。
• 对目前互联网协议的不满及对更好协议的期望。