snarks和iPhone之间有什么区别？ 当手机出现时，向现代人解释它是什么相对简单：它就像有线电话，但没有电线，它很小，你可以随身携带。形态新——想法旧：人类之间的沟通。 Snark是一个新想法。即使计算机本身也是相对较新的想法。对大多数人来说，可证明的计算目前是一种心理战：为什么要证明，证明什么，给谁，等等。 它甚至没有接近“如何”的问题。我们仍然处于根植这个想法的阶段，而不是它的实施，我认为我们做得很糟糕。 因此，在没有投资于整体可证明计算的根植思想的情况下，建立越来越多的基础设施（广义上）来进行可证明的计算——从长远来看是行不通的。为了可行，这项投资应该非常大，并且意味着非常严肃。 把它想象成制药公司将新药推向市场。它应该在所有层面上解决：药房连锁、诊所连锁、公立医院、私人医生、最终用户（患者）、意见领袖、媒体等。 这不是自然而然发生的。回想一下Uber：在它成为显而易见的出租车选择之前，会有成千上万的人在购物中心向人们推销Uber的想法，一人一人地。 首先我们销售想法，然后我们可以继续销售具体的实施。