嚴格來說，我現在還和試算表的發明人 Dan Bricklin 一起維護 SocialCalc。我們剛推出一個使用 Lean、Dafny 與 LemmaScript 的版本。現在只要引入錯誤，它就能立刻失敗，不必等測試日後抓出問題。我們依靠不變量與經 Lean 檢查的證明，讓程式變成「攜證程式碼」（proof-carrying code）。所以，它真的會失敗得非常快。