最近电脑坏了，所以上周没法写文章，抱歉。
随着AWS Automated Reasoning Group的兴起，可以感受到了编程语言在工业界的影响力的加大（这不废话吗，这么多人都被吸过去了），顺带不久前看了github semantic的ICFP Experience Report，想了想可以写一写关于这些的内容。
这方面一写paper是(缩写C)，讲coverity的程序分析框架在应用的时候的问题，<Fusing Industry and Academia at GitHub (Experience Report)>(缩写G)讲github内部的程序分析框架semantic，还有(缩写A)，讲AWS如何利用SMT solver对云上控制权限的验证。
其实ACG三篇paper都有很多共通点，我觉得与其一篇篇介绍，不如对ACG做一些总结
为什么要整X?
A:没说
C:我们一开始是为了publish paper，在几百万行代码上抓了很多错误，publish了paper以后，就觉得可以搞个大的。开家公司，请几个销售员躺着数钱钱，当然这考虑完全错误
G:做一个更好的，知道语义而不是只知道unstructured text的git diff
有没有遇到什么克苏鲁问题？
A:没有
C:好多，惨惨，哭哭。有一次我们跑用户的make，结果用户用了个奇奇怪怪的make语法写path，结果在蝴蝶效应下变成了rm -rf *。用户经常会给我们奇奇怪怪，不符合C语言标准的程序，然后因为各种原因无法改C编译器，最后要我们改自己的C parser。还有一次，给用户抓出use after free error，用户说free了以后还没malloc，所以freelist没有被复写，可以继续用，气死偶嘞！（整篇paper都是各种这些克苏鲁问题）
G:没有，卧槽free了后依赖于没有malloc继续用也太克苏鲁了
有没有遇到什么不克苏鲁的问题？
A:
我们遇到的最大问题是只有很小一部分用户会写SMT Query或者First Order Logic。但是，AWS有一百万用户，没有办法教这一百万个用户都写SMT。所以，我们把问题反转过来 - 对于一个输入（系统设置），我们会返回所有的信息（对于所有最终用户X跟数据Y，X能不能访问Y）。这时候，AWS用户只需要检查这些访问权限报告，就知道行不行了。
我们遇到的另一个问题是，当我们升级我们的SMT solver的时候，有的时候以前能Solve的Query会timeout，于是对一些用户来说，以前行的东东就不行了。我们的解法是，弄一个大大的portfolio，各种solver version都丢进去。
C:
我们也一样有软件升级问题。当我们升级完我们的静态分析器的时候，我们往往能抓更多错误，但这是不好的！更准确的说，我们的PM往往都想要一个这样的故事：‘我们引入了静态分析器，然后发现了X个错误，然后在过去Y个月里面，我们把这X个错误一步步消除掉！现在，我们的程序没有错误了！’，然后当他们升级软件的时候，错误越来越多，就会很气气！
另一个问题是，用户会不停提交代码，而如果你以前报过一次错误，同样的错误就不要再报了。我们写了一个错误database，然后会把所有分析出来的错误跟这个一一对比，只报告新的。
还有一个问题是，当我们报错误的时候，用户有时候看不懂，然后就会把我们的错误看成误报。当用户认为我们误报的时候，就会更不信任我们的工具，于是下次我们报错会更可能认为是误报。于是，我们需要很好的错误信息，并且对于一些复杂的静态分析，给出好错误信息更难，如果我们给不出好错误信息，我们宁愿不要这个分析。
G:
我们的新git diff能给出很有用的summary，于是得到了更多momentum（大概是有更多资源招程序员整这个）。但是用户不想安装跟用我们的新git diff。我们只好弃掉这个project。
更具体的说，我们不做git diff了，我们用我们整的静态分析工具弄一个Code Navigator，当你指定一个函数的时候，我们用静态分析找出这个函数用在那。
总结：
我觉得这三个工作都有一个共通点：如何包装销售自己的工作(Story)很重要。这里的销售并不是’口才很好‘的意思，而是’向谁卖什么‘。对于A用户来说，他们甚至不知道什么是SMT! 这时候，这整个工具就相当于’隐形‘的，需要跟用户打交道的地方小了很多（只剩下保证版本不会regress）。C用户会不停看到Coverity的工具，于是要求也最高。G也一样有这个问题，但是他们明白Story是可以改的，于是换了一个就好了。
当然，C的方法并不一定更’不好‘ - 在一些时候，这可以抓出’关键的错误‘，而semantic则做不到这个（因为已经包装成不是抓错误工具了）。更重要的是，C引入了一个叫’话语权‘的概念。当你的工具刚刚引入的时候，大家都不知道你的工具是做什么的，也不信任你的工具，于是会e.g.把错误看成误报，不看错误，或者就e.g.不会升级，或者买静态分析服务。所以这里有一个很典型的网络效应 - 在前期要给出很多精力去一个个服务用户，但是后面工具变出名了以后就不需要了。C也说了一句‘好日子在后头’之类的话：在以前静态分析没有C的时候这么流行，于是它的前辈要做的斗争更难。可以预想的是，很多这些都是‘一次性开销’，后续工具的应用会更简单。
另外，Github：Haskell真香，ICFP是我的秘密武器！