大尺度做爰网站/整合营销传播工具有哪些
原标题：计算机编程犹如我们掌握语言是未来社会的基本条件
我们的处境是，我们已经站在了一个通向「写正确的程序」的路口，这条路看上去十分曲折，但里程碑已经显现，待我们去探索。
因此，答案可能是某个支持 Dependent Type，支持 Programming/Proof by Refinement 的语言插上一大堆做 Term Unification / ATP 的插件……
Dependent Type：允许程序员以简单直接的方式约定他想要写的程序应该满足的性质，并且可以以以下方式确保：形式证明之，如我之前写的例子；Property-based Testing，这个和形式证明相似，只不过是通过运行大量随机生成的测试案例检验性质是否满足；传统的单元测试。
三者的成本逐渐下降，正确性也逐渐下降，但是三者结合，便平衡正确性与成本。除证明测试外，Dependent Type 带来的强大类型描述能力也可以将入口细化，降低程序员出错的概率。
Programming/Proof by Refinement：允许程序员以逐步细化的方式实现非常复杂的约束。比如
@雾雨魔理沙 那个 DeepDarkFantasy 里面有这样一个类型非常吓人的函数：
hlam::forallreprabh.DBIrepr=>((forallk.NT(repr(a,h))k=>ka)->(repr(a,h))b)->reprh(a->b)
(ps.
@雾雨魔理沙 说把 DDF 换成 Haskell 是她这辈子做过的最正确的决定 orz)
一般人看到这个估计都晕倒了吧，不过使用类似于 Coq 的 LTac，写出来并不算非常困难：
-- TTS -- under designhlam : {repr : Type -> Type; a, b, h : Type | DBI repr} -> (({k : Type -> Type | NT (repr (a >< h)) k} -> k a) -> repr (a >< h) b) -> repr h (a -> b)-- this type is scary, but we have tacticshlam = tactic { (repr,a,b,h) < h) a -> repr (a >< h) b x < h) b apply f -- ... |- {k : Type -> Type | NT (repr (a >< h)) k} -> k a k < h) a exactly x}
在搭建的过程中通过一点点拆解复杂的目标，最终写出整个程序出来。上面的「Tactic」看着玄乎，实际上只是搭积木一样的过程而已。
Programming/Proof by Refinement 的过程实际上还可以和 Property-based testing 结合，比如如果某一步中出现的 goal 或者 assert 测试不过，那么就可以直接在交互界面显示出来，等等。
Term Unification / ATP：如果 Programming/Proof by Refinement 还是觉得麻烦怎么办？别忘了上面的 Tactic 是一块块的积木，那么能不能写插件去自动地把积木拼上呢？如果结合现在发展迅猛的人工智能呢？
总上而言，我们离「写正确的程序」已经越来越近。如果说编程有未来的话，这个才是值得期待的未来。返回搜狐，查看更多
责任编辑：