程序語言理論學術界的工作在工業界有哪些應用？
我以下的答案是姚培森同志答案的補充。
除了姚大提到的很多知名的公司和產品，很多企業（Microsoft, Oracle, IBM, Google, Facebook之類）都有自己內部的分析，測試，驗證工具（由自己的研究團隊設計開發，或部分和高校尋求合作），支持著整個公司很多軟體產品的生產。這些工具從某種角度來說對自己公司的產品更有針對性，因此有著更好的實用性，切實地提高了公司生產力，節約了很多的成本。這些產品背後的理論支持也都逃不過PL的很多概念和方法。所以說，持PL是學術界自己玩並沒實際用處觀點的人，請慎言啊。當然我個人認為，PL研究的意義也遠不是為了給工業界省點錢，和所有的research一樣，它是一種自由的東西，是可創造，可欣賞，可以不可思議的東西（當然也可以吐槽，為什麼不呢，學術八卦很有意思的）。
另，我同意姚大的看法，這些理論不是故意讓人看不懂的。它們本身用來抽象地描述很多很複雜的系統（編程語言），想要描述的正確、準確並能證明很多衍生出的性質（很多性質在實際當中也很有用），必須要用一些符號和相關的理論框架來支持描述。畢竟數學語言總比人說話來的簡潔、有效並少有歧義。慢慢地，這些看似複雜的符號系統已經變成高效準確地表達很多PL方法的通用「語言」了。一個發展了幾十年的領域，搞的人一直都是不多的，你還不讓人家自己有點自己的交流系統，這不太像話吧。而且圈子不同，態度也不同。很多SE（軟體工程）頂會ICSE/ASE的paper裡面的陳述，放在PL的頂會很有可能是要被斃掉的，因為不準確不嚴密。
拿PL中的程序分析舉個例子，你說你的分析方法是sound的（暫且理解為正確吧），是什麼條件下sound啊，所有語言特性都支持嗎（軟體不是用語言寫的嗎），多線程？native方法？如果是OO語言，reflecion和dynamic code loading呢？C/C++的pointer arithmetic operations? 還有其它語言的一些神煩的特性。
有的人說，以前很多論文都不提啊，那是因為是以前的論文，現在程序分析是什麼境遇啊，是生長期實用期啊，人家要用你方法的人是按需期待的啊，他要知道用了你的方法，會有什麼樣預期的結果。我上面提的語言特性你不說什麼條件下sound，下面這些問題你就沒法回答，甚至會大大地影響結果。例如，報出來沒有錯就是真沒有錯嗎（驗證），報出來100個錯就是100個左右的錯嗎？優化不會優化錯嗎？百萬級的程序在標準library下你的分析程序能跑完嗎？大概多長時間？等等等等。此外，從research的角度來看，你說你方法就是sound了，而且還能保持你文章列出的那麼好的分析精度，那麼以後的人怎麼繼續做啊，你都搞定了，路都被你走完了（實際上沒有）。這樣不但堵住了同行的路，從research本身角度來講不嚴謹，不準確，從實用角度來講，指導意義和實際可操作性也不強（總不能讓用你方法的人實現一下放在自己的工具鏈里，最後發現不是那麼回事吧，公司不會這麼乾的，燒錢啊）。所以像這種claim方法的key features時，要準確嚴謹。我就在這上面吃過教訓，跟別人交流過大家也都有類似的經歷（所以有時發PL的文章累啊）。
我說這麼多就是想說一下，大部分情況下，在論文裡面描述準確、嚴謹，尤其是在PL領域是一種必須。據我所知，很多好的文章都是因為說話不嚴謹（包括在實驗階段對結果的描述和分析上不嚴謹）被斃掉的（因為很多reviewer很在乎，尤其是PL的人），比如某年一篇被PLDI斃掉的文章馬上投到了SE頂會FSE得了個best paper（我可沒有說FSE比PLDI差，個例而已，而且這篇論文無論從idea還是結果上看都很不錯）。
不知不覺嘮叨了這麼多（敘述邏輯也不好，想啥說啥），看客抱歉了，我就不從新整理了。
總結一下就是PL(T)還是有很多實際用途地，它也不是故弄玄虛地讓人看不懂地（不要聽某些「大神」一家之談，當然也要用批判地眼觀看我這個nobody的答案）。我也不是上來就對PL有好感的（我是單純地對學術有好感），但是慢慢接觸下來（我接觸過SE，compiler和System），發現PL這個領域是一個值得讓人尊敬的，越挖掘越有好感的（因為理論很深，知識體系的積累並不是經驗型的，而是結構型的，這樣會有一種打怪升級不想放棄的感覺）研究領域。因為研究的人比較少，開會的時候就有它的好處，因為你那為數不多的聽眾里有著你以前各種在傳說中聽到的人（各種語言之父，業界大佬），還有很多意氣風發的年輕面孔，讓你突然感到「人們在知識下的純粹」，讓你漸漸感到「我想做的更好」。於此，PL能讓我漸漸喜歡上它（儘管現在還不能說很喜歡），並讓我有想為它做一些事情的想法和行動，於我（這種初學者）和那些已經在PL領域裡奔波的人們而言，也不失為一種應用吧。
以上。舉幾個例子：
編譯器：Chez Scheme, Glasgow Haskell Compiler(GHC)!
程序分析：Coverity, Grammar Tech(主要產品CodeSonar), Astree程序生成：Flash Fill(集成在Office 2013)程序測試: SAGE程序驗證: SLAM語言設計：Rust的affine type, regine type，Type Script, Python的gradual typing..
定理證明: Coq, Isabelle, ACL2, Z3......程序語言相關的研究很廣，都有其理論和實踐部分：- 偏向System/Arch/Security的：並行、系統安全等，相關會議：ASPLOS、OSDI/SOSP, NDSS/SP/CCS/USecurity..)
- 傳統Compiler向的：CGO，CC等
- 有側重於Software Engineering的：ICSE、FSE、ASE等（PS: Software engineering各種提神醒腦的應用多了去了...
- 話題比較小的：ISSTA, SAS, PEPM..
- 有重點關注Verification/Formal method的：CAV, TACAS, VMCAI, FMCAD，更理論的LICS, ICALP..
- 綜合性的: POPL, PLDI, ICFP, ECOOP, OOPSLA..
推薦閱讀：