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), 可以看看.