神刀安全网

回应CFA传人对我的攻击

发表了之前的文章《 我为什么不再做PL人 》之后,我发现有人(其实是一位CFA技术的传人)在知乎上发表文章黑我。本来不想理知乎上的东西,但作者把各种刚从论文上学来的术语,似懂非懂写了一大堆,挺能唬人的,所以我只好回应一下。现在我把这篇文章的 链接 放在这里。评论的第4页有我的回复,技术性比较强,不过有兴趣的人可以看看。为了方便,我也把评论拷贝到这篇文章末尾。

文章作者彭飞的导师是Jens Palsberg,其实就是曾在CFA领域做过研究的一位学者。我本来对Palsberg没有意见,因为他的研究不只限于CFA。Palsberg还跟我很尊敬的Neil Jones教授做过很多其它方面的研究,所以我无意与他为敌,也从来没有在批评CFA的时候点过Palsberg的名。但由于我指出了CFA领域的弊病,彭飞恐怕就是一心一意研究这个的,所以觉得“祖业”受到了攻击,想要反驳我,支持CFA的“先进性”,这样以后可以在学术界更好的混下去。这可以理解,然而彭飞的文章,其实破绽百出,这些都从我的评论里可以看得出来。

CFA领域的理论从来没有成功实现,展示过它的功效。CFA最强大的版本,CFA2和P4F的作者Dimitris Vardoulakis,当年在Mozilla实习的时候试图在JavaScript上实现CFA2算法。最后的产物叫做“DrJS”,还做了一个网站让人试用。可是在不久之后DrJS不了了之,消失了。后来跟Mozilla的research director聊天时,他告诉我DrJS其实根本不好用,理论过度复杂,实现起来非常困难,而且达不到号称可以达到的效果,说Mozilla以后不想再赞助类似的项目了。之前在Sourcegraph的时候,两位founder也试图采用DrJS来做JavaScript的分析,后来发现不好用,改用了 tern 才产生了有用一点的信息。

PySonar2比CFA2,P4F都要强大的原因很简单,因为它根本没有CFA所用的continuation passing style(CPS变换)所带来的所谓“call/return匹配问题”。所有的call和它们的return,被abstract interpreter自然而然的匹配好了,根本不可能错位。我很惊讶的是CFA领域研究了20年,就在解决这种根本不存在的问题。彭飞抓住PySonar2表面上的一些小问题指指点点,貌似好大个事情,而其实很多都是由于他自己理解不够深入。详情请见我的评论。

另外,我真的对Python,Ruby,JavaScript这些动态语言做type inference不感兴趣了。PySonar2虽然比CFA简单和强大很多,但是我从来没想维护PySonar2的“先进性”,我从来没想推广PySonar2。因为我根本不在乎Python,也没把PySonar2当回事。给Python这样的语言做一个很好的类型推导工具,有什么意义吗?未来的方向是直接写上type annotation,就像Java和C#那样,让类型检查简单,迅速又准确。所以PySonar2和CFA领域做的其实都是无用功,只不过我没花20年时间研究CFA,只用了加起来几个月时间,而且还比他们做得更好。

彭飞错误地认为我很把PySonar2当回事,然而它只是我曾经做过的一个小玩具。我一直在探索和展望更加实在,对人可以产生真正效益的领域。只是随便提了一下CFA,就得到如此强烈而具体的攻击,我对PL人士的自我保护意识真的很惊讶。如果你观察到彭飞似乎对PL刚入门,在知乎上发表挺多入门级的PL文章,而且看CFA的论文也才不久,也许会意识到,他其实是想在知乎上建立自己的“权威地位”。由于最近研究的CFA受到了攻击,想要重新树立起小白们对于CFA的崇敬之情,倒也可以理解。知乎,真不愧是民科的天堂 :)

以下是我评论的内容,可能会略有改动:

不要以为我不上知乎你就可以随便胡扯。你的导师Jens Palsberg就是那帮CFA扯淡的人之一,你当然那么说了。CFA2的发明人在Mozilla做的那个东西(DrJS),后来发现根本不能用(Mozilla research director亲自跟我说的),所以现在网站都消失了。

Pushdown Control Flow Analysis完全干的就是PySonar2很简单就能完成的事情,而PySonar2根本不需要什么pushdown automaton,完全依靠自然的abstract interpreter call/return。你们2016年才发那样的paper,PySonar2早在2010年就解决了这个问题。

另外那几个链接没有指向,是因为当时在Sourcegraph,他们需要一个fully qualified name,所以没法再同时指向两个地方。然而实际上reference其实都是有的。至于Hindley-Milner那种generic type的抽象,对于Python这种非常polymorphic的语言是不可行的。简单的a->a可以,但是控制流复杂一点就不能再有效。

另外,我真的对这种动态语言inference不感兴趣了。PySonar2虽然还是比你们的CFA先进很多年,但是我从来没想维护PySonar2的“先进性”。给Python这样的语言做一个很先进的工具,有什么意义吗?未来的方向是直接写上type annotation,就像Java和C#那样。所以我们做的都是无用功,只不过我没花你们那20年,而且还做得更好 😉

另外我在2014年末的样子给CFA的“鼻祖”Olin Shivers写了封email,寻找合作机会。讲述了我的PySonar2的做法,而且问他为什么他的call/return match用那么复杂的方法来做。如果他们的2016论文加入了我的想法,也不足为怪。但是真的不care这些了。你们学术界随便胡搞好了,反正也不可能有什么用处。这些东西做static analysis的人早就明白,CFA远远落后,只能在自己的圈子里发表点paper。

另外,推导出的 {int -> int} | {bool ->bool}表示的其实是一个intersection type,而不是union type。我不知道你到底明不明白什么是intersection type。这个type表示这个函数“同时”是int->int和bool->bool,而不是表示“有时”是int->int而另外的时候是bool->bool。这是对于Python最多能做到的事情。

你说的forall a. a -> a对于复杂点的Python代码是不可行的。PySonar做过HM那样的系统,能推出forall a. a -> a那样的类型,但是后来发现遇到复杂点的代码根本不可能准确的generalize。有本事你用CFA给我们show一下推导出forall类型?我随便写段代码你的推导就完蛋了。

我从来没说过PySonar2是sound的。其实你们的CFA2和P4F,对于Python也不可能是sound的,因为本来就是undecidable的问题。这些工具能做的,只是最大限度的发现类型错误而已。它们并不能完全排除类型错误。

不得不引用一下Linus的话(虽然我鄙视这句话):Talk is cheap. Show me some code。你把CFA实现出来,给我们show一下它能生成什么样的结果?哈哈。CFA2的发明人已经在Mozilla试过了不是吗?过度复杂的理论,根本不能实现和work。

转载本站任何文章请注明:转载至神刀安全网,谢谢神刀安全网 » 回应CFA传人对我的攻击

分享到:更多 ()

评论 抢沙发

  • 昵称 (必填)
  • 邮箱 (必填)
  • 网址
分享按钮