＞サーストンはコンピューター大好き人間だし

それは形式化大好きということとは違う。

＞機械を使った証明検証に対する彼の好意的な意見は
＞http://arxiv.org/abs/math.HO/9404236
＞に述べられているから読んでおくように。

君こそちゃんと読んだほうがいい。
彼がフォーマリズムを信頼してないことが分かる。