它的口號是讓機器自動生成符合要求(功能要求、安全要求)的代碼，生成的代碼經過形式驗證。理論上，經過正式驗證的代碼不需要編寫測試。程序員不再需要絞盡腦汁去思考測試用例。因為機器幫助我們驗證程序的行為在所有可能的輸入下都符合要求，所以這種保證是極其強的。如果無人駕駛汽車的控制程序中有壹個變量叫做distance_to_wall，然後我們生成的代碼保證這個變量永遠大於0，那麽我們就有了壹輛不會撞墻的無人駕駛汽車。但是現在技術還沒有那麽成熟，但是科學家們正在努力。
結果大家都是產品經理，提要求就行了。對於壹直追求極致自動化的計算機科學家來說，這個未來是多麽的誘人。素描是壹個有影響力的項目，但如妳所說，它的應用還是有限的。
程序生成主要依賴於約束求解技術。每個人在高中都接觸過約束求解。解線性方程組就是約束求解的壹個例子。SAT問題也是約束求解。我們可以發現，約束求解並不是壹個算法，而是壹個非常籠統的名稱。對於不同的約束，其實有不同的決策程序。可滿足性模塊理論技術是集成不同求解算法的框架。我的朋友，卡內基梅隆大學的Sicun Gao博士和Soonho Kong博士開發了壹個叫做dReal(dReal)的SMT求解器，它支持約束中的微分方程。巧合的是，四村高現在正在素描作者所在的實驗室做研究。
程序生成的技術大概就是把源代碼轉換成壹個約束表達式，“”轉換成壹個未知變量，然後扔給約束求解器，求壹組解。加州大學柏克萊分校的拉斯博迪克教授開設了程序生成課程(拉斯博迪克-EECS)，可見壹斑。