sketch编程

❶ 怎样看待“智能化编程语言”Sketch

这属于程序生成(Program synthesis), 是形式验证(Formal verification)一个偏应用的分支.

它的口号就是能够让机器自动生成满足需求(功能性需求, 安全性需求)的代码, 并且生成的代码经过形式验证. 经过形式验证的代码, 理论上不需要写测试. 程序员再也不用绞尽脑汁想测试用例了, 因为机器帮我们验证了在所有可能的输入下程序的行为是合乎要求的. 这个保证是极强的. 假如无人驾驶车的控制程序里有一个变量叫distance_to_wall(车到墙的距离), 然后我们的生成的代码保证这个变量永远大于0, 于是我们就有了一辆不会撞墙的无人驾驶车了. 但是现在的技术还没有这么成熟, 不过科学家们在努力.

这样的结果, 人人都是产品经理了, 只要提需求就好了. 对于一直追求终极自动化的计算机科学家来说, 这样的未来是多么有吸引力啊. Sketch就是做得比较有影响力的一个项目. 但是如你所说, 应用还是比较有限.

程序生成主要依赖于约束求解(Constraint Solving)的技术. 所有人高中都接触过约束求解. 求解线性方程组就是约束求解的一个例子. SAT问题也是约束求解. 我们可以发现约束求解并不是一个算法, 只是一个很笼统的称呼. 对于不同的约束, 其实有不同的求解算法(Decision procere). Satisfiability Molo Theories技术是把不同的求解算法集成起来的框架. 我的朋友, 卡耐基梅隆大学的Sicun Gao博士和Soonho Kong博士开发了一个SMT solver叫dReal(dReal), 支持约束条件里有微分方程. 很巧的是, Sicun Gao现在就在Sketch的作者所在的实验室做研究.

程序生成的技术大概就是将源代码转化成一个约束表达式, "??"被转化成未知的变量, 然后扔给约束求解器找出一组解来. 加州伯克利大学的Ras Bodik教授开了一门程序生成的课(Ras Bodik - EECS), 可以看看.