如何评价微软研究院的Dafny语言

2019-11-08 20:52:52

刚写了一个Dafny的简介Dafny与程序验证从程序语言的角度来看,Dafny的设计还是比较Modern,比较优秀的。它结合了OOP和FP,ADT是Haskell的写法,比Scala更简便。有命令式的method也有函数式的function,总之就是怎么爽怎么写,还可以编译到C#。MS家的PL组合拳C#+F#+Dafny简直可以让你上天。但是,它的缺点也有不少,比如ADT不能深层匹配,只能一层一层地匹配(可能是为了Verify更方便);对OOP的支持不如Scala好;库和语言不分(可能也是为Verify方便Orz);以及,最致命的伤,没有标准库。编译器有很多Bug我就不说了,不属于评价编译语言好坏的范畴。。。从程序验证的角度来看,Dafny应该算中等偏上。我目前玩过Boogie,Z3,Dafny和Scala家的stainless(以前叫leon),有的问题在这个语言好证,有的问题那个语言好证。不过Dafny有一点很强,它可以验证Dirty的代码,这一点Scala选手表示已经跪了。但是,Scala的stainless在验证不通过时可以构造反例,leon(目前正在逐步迁移到stainless)还可以给出正确的代码实现,这确实是很吸引人的地方。不过stainless启动太慢了(这个赖scala╮(╯▽╰)╭还有,Dafny的IDE支持比stainless好,stainless居然想让我们用eclipse写代码,天呐,没有idea怎么活!以及,dafny有languageserver,可以一边写代码一边看验证结果,stainless那边开了个sbt插件的branch都开了几年了,还没有推出正式的sbt插件,我都看不下去了,自己撸了一个从外部调用stainless的插件,牺牲了一(hen)点(duo)速度。另外,程序验证真的是玄学,你根本不知道要给Verifier写些什么hint,它才能证明出结论。这一点上述verifier一个都没跑。

上一篇:如何评价五年级小学生周一周五请假来复旦旁听课程这一新闻_3
下一篇:没有了

Copyright(c)2003-2033清大教育在线All Rights Reserved
地址:北京市海淀区上地信息产业基地
网站地图