標籤：

研究編程語言的人們研究哪些方面？

12-27

王垠的博客里寫的那些片段覺得好有意思,
http://blog.sina.com.cn/s/articlelist_1569777711_0_1.html
然後研究編程語言的人研究些什麼東西呢?

補充 @邵成的回答

在PL相關的學術界

  • 有偏向System/Arch的：研究並行、功耗、安全等，相關會議：ASPLOS、OSDI/SOSP
  • 有主要玩Compiler黑魔法的：PLDI，CGO（這個會不太好）等
  • 有側重於Software engineering的：研究程序切片、安全等，相關會議：ICSE、FSE、ASE等。
  • 有重點關注Verification/Formal method的：model checking, hoare logic等。
  • 比較「正統」的PL理論相關的：POPL是首選。其他如ICFP、OOPSLA也很好，PLDI也有比較理論的文章。

個人認為比較突出的幾個華人：

胡振江（Zhenjiang Hu）
他算是最「傳統」的，而且涉獵甚廣。據我有限的了解，同時發過POPL、PLDI、ICFP、ICSE、SAS的人真不多。。

邵中（Zhong Shao），耶魯FLINT實驗室老闆。
形式化相關，VeriML等項目非常有影響力。近年來似乎不太活躍了。。值得一提的是，他還參與過SMLNJ的開發！（相信不少玩Standard ML的人用過）

Song Dawn（Dawn Xiaodong Song）
偏向系統、安全。和PL相關也說得過去。。真.女神。

國外大師級的：

Philp Walder（Philip Wadler）
前Sigplan主席，Haskell語言真.靈魂人物。

Robert Harper（Robert Harper）
真.Robin Milner傳人。。還培養了Morrisett、B.Pierce等一批後起之秀。如今繼續為Homotopy Type Theory開疆拓土

Luca cardelli（Luca Cardelli）
Object calculus的提出者..現在玩起Quantitative Semantics、Molecular Programming了（你們這些搞OO的（逃

歡迎補充。

-----------------------------我是分割線---------------------------------------------
那麼問題來了，到了王垠話題

垠神和他所推崇的D.Friedman有些類似的特質，會當老師且文筆不錯，能把基礎而本質的東西講清楚，這點很難得。我個人從他的文章里學到不少東西。

另外根據他之前的言論以及在知乎的回答（已經刪了）不負責推測，垠神形式語義學得不好（並且對此有不屑一顧的傾向），系統/體系結構相關的功底欠佳（用本領域的經驗/理論指導一切的想法可能導致偏頗甚至偏執）。。

至於他在PL學術界算什麼水準，我不好也沒有能力評價。（民科？合格的博士生第二年水平？大師級只是不想寫論文？）確定的是，王離開真正的PL學術圈子已經挺久了。

無意中看到姚大 @姚培森 的回答，很多我贊成，但是有幾個關於學術會議的，我有些想提一下個人看法，以便在大家選會議和文章閱讀上有一個更豐富的參考。

第一，關於compiler黑魔法那個，說CGO這個會不太好，有些不太合適，這個會現在的競爭力很大，CC已經被它甩到後面去了，你可以看一下近年來錄取的文章的機構，都是很重量級的，尤其近來年北美越來越青睞它。編譯的CGO的地位就相當於軟體工程的ISSTA，搞編譯的人CGO是必選的硬會。

SE方面，沒有提ISSTA。它現在的地位比ASE要高了，近兩年文章平均受關注程度在SE里也非常高。尤其是在PL方面，很多論文側重結合語言來討論分析和測試方法，所以SE的會，ISSTA建議提及一下。

關於PL的會，雖然我副導是靠oopsla發家的，但是搞語言的人，尤其是搞OO的，肯定先提ECOOP。語言理論的影響力ECOOP是僅次於POPL的，這不是我說的，這是好多搞語言的人說的。

題外，接姚大說的王垠學術話題。

發一篇頂會不是寫一篇文章，很多情況下你既要跟世界上最懂的專家博弈，招架來自他們從各方面可能發現關於你方法或理論的漏洞攻擊，還要顧全非專家的人把你的文章讀懂，並且讓專家和非專家都說你好你行你這有用你這靠譜，此外全世界這麼多聰明的人在一起競爭這麼有限的錄取數量，而且一切的一切都在這麼有限的幾頁紙裡面說清楚道明白，尤其是語言這麼複雜的系統。這些是能力，我相信是需要靠經驗和反覆訓練才能練就的能力。
我不了解王垠，但是我堅信他學術上還沒有到能不屑發頂會paper的水平，很簡單，因為他沒有一篇這樣的paper，我不信他有這樣的水平。但是看到這麼多優秀的學生像 @姚培森@邵成都受過王垠的影響，還有很多學生是因為王垠而想嘗試語言的學習，儘管有很多人黑他，我又由衷的覺得王垠很成功，很有魅力，是的，我是男人。

所謂「研究編程語言」，範圍其實是比較廣的。看看今年PLDI的Call for papers就知道咯（POPL的太籠統，就給了個Scope）
Papers are solicited on, but not limited to, the following topics:

  • Language designs and extensions
  • Static and dynamic analysis of programs
  • Domain-specific languages and tools
  • Type systems and program logics
  • Program transformation and optimization
  • Checking or improving the security or correctness of programs
  • Memory management
  • Parallelism, both implicit and explicit
  • Performance and energy analysis, evaluation, and tools
  • Novel programming models
  • Debugging techniques and tools
  • Program understanding
  • Interaction of compilers/runtimes with underlying systems
  • Program synthesis

最理論那就基本上是數學了，極限早就被祖師爺框死了，我不知道還有什麼搞頭。

還有研究語義的，研究指稱語義抽象機語義等等 實際上是把程序語句對應到某種數學模型，是為語義；再往下一點是Type system，研究不同類型系統的作用和限制，或者設計牛逼的類型系統可以自動推導很複雜的類型。

但這些東西搞得累死累活，做出來的東西工業界的程序員基本用不了。所以上面那些東西很少人搞了，大家都搞些更有實際作用的東西。程序語言有五大頂會：
最難中的POPL PLDI最雜，什麼都收，所以競爭最激烈。
OO的有正宗的ECOOP和本來也正宗現在為了擴大影響力開始收些非OO文章的OOPSLA。
Functional的有ICFP。
如今時代在變，往前退個五六年，POPL和ECOOP很多論文都沒有實驗，現在這都玩不轉了，大家都想看看你的新成果有什麼用。這些會議的改變或多或少主導了熱門研究方向的偏向。

比如再具體一點有model checking和verification，研究如何給一個程序建模然後通過分析建好的模型來查錯；優化，這個不用說了；拓展程序語言，比如有些論文的結論就是給語言加個關鍵字就能避免程序員寫出某類bug（那位做relaxed memory model的老兄應該也算這類，而且還有些model checking的意思）；再然後，就是我們搞的程序分析啦！

搞分析當然是研究語言啦，不研究語言怎麼做分析器？所謂分析，這裡尤指靜態分析，作用是分析出程序的某些屬性，這些屬性可以有很多用處，主要是優化和查錯，工業界更為重視錯誤，所以可以說做分析的就是和bug死磕。做分析的人做夢都想要搞出一個分析器，恨不得把真實程序里的bug全部逮著，還沒有false positive。當然這是不可能的。

靜態分析有什麼好研究的呢？那簡直多了去了。舉個經典問題：指針分析，也就是分析程序里的指針在動態執行期間可能指向哪些(abstract) objects。知道這個結果可以干很多事情。就這麼個描述起來那麼簡單的問題，以Java為例，學術界搞了十幾年都沒做出一個公司能用的指針分析。基本上要麼太慢（我們發論文，一個程序分析一天都是可以接受的），要麼太不準。除此之外，如何處理dynamic class loading, native method等語言特性對靜態分析的影響，至今仍是懸而未決的難題，而這種硬骨頭又很少有人願意去啃。

此外編程語言的研究通常與軟體工程領域緊密相連，國外有些研究組就叫pl and se group，所以一點不奇怪有人既發PLDI又發ICSE。

所以在我接觸到的範圍內，研究編程語言就是研究怎麼去查錯，優化，幫助公司和程序員生產更好的軟體。當然編程語言也可以搞得飛起，比如有位仁兄提到的Luca cardelli,去年去ECOOP的時候聽他講他們的分子編程，簡直跟OO沒有一點關係，已經超出一般語言的範疇了…

Strategic directions in research on programming languages

96年的文獻綜述，略舊，不失為不錯的參考。
@姚培森譯稿：Strategic Directions for Research on PL(draft)

（原諒我中英夾雜……很多時候夾雜的原因是因為那個詞翻譯過來的感覺不對，比如說 expensive 翻譯過來是貴，但是我想表達的意思是時間上很貴或者代價很大……還有一些是我不知道如何用中文表達）
講個具體的例子，介紹一下我目前在做的吧: Relaxed Memory Model, 很多人沒聽過這個詞，不過可以算目前 PL 領域比較熱的一個話題之一，看最近幾年的 POPL 上都有這個方向的文章（當然大部分是我們組發的哈哈）。

首先看個例子：假設有兩個（physical） thread, a 和 b 在開始的時候都是0
t0 | t1
a = 1 | b = 1
r1 = b | r2 = a

請問如果我們兩個 thread 都運行完後把 a 和 b 列印出來，結果會是多少？ a = 1 b = 1； a = 0 b = 1； a = 0 b = 1； 都是合理的答案，但是 a = 0 b = 0呢？ 很明顯如果從邏輯上來說是不可能的（如果不理解這一點的話，可以自己試著寫一寫在運行這兩個 thread 的過程中所有可能出現的 statement 被執行的順序，然後看看最終的結果，提示：a = 0 b = 0 ===&> r1 = b 或者 r2 = a 被 reorder到a = 1 或者 b = 1的前面）。

但是在真正的硬體平台上（x86, power, ARM）我們是可以觀測到 a = 0 b = 0 這種不應該出現的結果的，為什麼呢？ 因為在現代的處理器中，因為寫內存是很 expensive 的，所以所有的 store 都會被先存到一個 store buffer 裡面，然後在未來的某個時間點 propagate 到 main memory。如果處理器需要讀取某個內存地址，它會先查看自己的 store buffer 裡面是不是包含這個地址，如果包含就直接從 store buffer 裡面讀取，如果不包含再讀 main memory。這樣的設計對單核的系統是沒有問題的，但是對多核系統，比如上面那個例子，a =1 和 b = 1分別被寫進了兩個核的 store buffer， 然後兩個 read 分別從 main memory read，就會造成 a = 0 b = 0 這種奇怪的結果。

因為現代處理器中有很多這種針對單核系統的優化，所以當多核時代到來，這些奇怪的結果出現的越來也頻繁，人們就統一給這種現象取了個名字：叫 relaxed memory behaviours，為什麼叫這麼個怪名字呢，因為其實很久之前有位大神，Leslie Lamport (ACM Turing Award 2014) 想過這個問題，他提出了一種關於多核計算式 memory model 應該提供的性質，叫 Sequential Consistency，這個定義我就不翻譯了（能力有限），貼在這裡：

... the result of any execution is the same as if the operations of all the processors were executed in some sequential order, and the operations of each individual processor appear in this sequence in the order specified by its program.

但是現實生活中的處理器都是一般不能提供這種很強的保證的，在不使用 atomic operation 和 memory fences 的情況下， 他們可以產生很多不同的relaxed memory behaviours。再舉個例子，還是假設在 program開始的時候 a = 0 b =0
t0 | t1
a = 1 | while (b == 0)
b = 1 | r2 = a
實驗證明，r2 最後有一定幾率會是0，這個例子是個很典型的 multithread programming idiom，叫 message passing，也就是說很多 real world system 是依賴於這樣的 programming patter，我們可以很容易想像 b 是個操作系統中的信號量，然後 a 是系統的某些設置……

那麼到了這裡你可能會想，那麼我們在合適的地方加上 fences 不就行了？比如上面這個例子，如果我們加上 fence
t0 | t1
a = 1 | while (b == 0)
fence | fence
b = 1 | r2 = a
這樣的話，r2最後的結果一定是1，這樣做的話有幾個問題, 第一是 fences 一般很貴，會對 performance 造成影響。第二就是，如果你去看 intel（Intel速 64 and IA-32 Architectures Software Developer Manuals）或者 arm 的手冊，且不說這些 specification一般都有上萬頁，就算你有耐心讀完，你會發現處理器提供各種各樣不同的 fences，而且他們對每個 fence 到底能做什麼，不能做什麼寫的非常含糊，雖然他們提供了很多例子（ 術語叫litmus tests，雖然這個詞有很多意思），但是這些例子也不能很好地展現到底什麼樣的 memory behaviour是應該被允許的。大部分這些架構的 specification 使用 plain English 寫的，但是在這些科技類文檔裡面，英語很多時候是不夠精確的，我們需要更準確的語言（數學語言，具體到這裡就是 operational，denotational 或者 axiomatic semantic ）去描述這些系統。而且 programmers 通常不具備很高深的計算機架構知識去明白為什麼有些 memory behaviour會出現，我們需要給他們提供一套更容易理解的 memory model，讓他們能夠預測自己的 code 會產生什麼行為。

而且以上說的這些只是談處理器和他們的 assembly language，其實 GPU 也有這些問題，同樣的，C 和 C++作為系統級語言，也需要 expose 這些 hardware feature，那麼什麼樣的 abstraction 是合適的也是個很有趣的問題。

所以我們做的工作包括以下一些：

  1. 把 specification 從英語轉換成formal mathematical definitions（具體到我自己是做 operational semantic）；
  2. 在 real world system 上做測試，看看他們的行為跟 specification 是不是 match，你可以很驚奇的發現有些處理器的行為其實跟他的 specification 是矛盾的；
  3. formal verification，C++ spec 裡面會有這樣的句子：如果你的 program 里每個 memory read 和 write 都是 atomic 的，而且都標記了 seq_cst，那麼你的 program 只會有sequentially consistent behaviour。這相當於是關於 C++ memory model 的一個 theorem，那麼我們如何驗證它呢? 我們從1裡面得到的數學模型就有用了，我們可以證明這個命題是成立的。當然一般不是全手工證明，要用到 isabelle 或者 coq, 有時會得到一些比較好的結果，比如發現 spec 裡面的命題是不成立的，這個時候就可以提一些建議；

現在人們越來越意識到，programming language specification 不是一個很簡單的工作，想做到讓你的 language consistent with itself 通常需要比較專業的數學知識，而且程序語言是一個比較大的系統，想做到系統內 consistent 需要做證明，而不是拍腦袋空想。所以現在的趨勢是不僅要 formalise part of a language，而是要 formalise it all。這方面也有很有趣的工作。

下面是一些 paper：

  1. http://www.cl.cam.ac.uk/~pes20/weakmemory/cacm.pdf
  2. http://www.cl.cam.ac.uk/~pes20/ppc-supplemental/pldi105-sarkar.pdf
  3. http://www.cl.cam.ac.uk/~pes20/cpp/popl085ap-sewell.pdf
  4. http://www.di.ens.fr/~zappa/readings/c11comp.pdf
  5. http://www.cs.cmu.edu/~crary/papers/2015/rmc.pdf
  6. http://fsl.cs.illinois.edu/FSL/papers/2015/bogdanas-rosu-2015-popl/bogdanas-rosu-2015-popl-public.pdf

PLT（Programming Language Theory）是個吃力不討好的領域，具體研究啥可以參考wikipedia:

http://en.wikipedia.org/wiki/Programming_language_theory

  • Formal semantics
  • Type theory
  • Program analysis and transformation
  • Comparative programming language analysis
  • Generic and metaprogramming
  • Domain-specific languages
  • Compiler construction
  • Run-time systems

為什麼說吃力不討好呢，因為這是個不多的民科盛行學院埋沒的領域之一。當然這是學院派那邊的吐嘈，比如Diva mm說的:

Is there still research to be done in Programming Languages?
http://tagide.com/blog/2012/03/research-in-programming-languages/

Since the 90s, a considerable percentage of new languages that ended up being very popular were designed by lone programmers, some of them kids with no research inclination, some as a side hobby, and without any grand goal other than either making some routine activities easier or for plain hacking fun. Examples:

  • PHP, by Rasmus Lerdorf circa 1994, 「originally used for tracking visits to his online resume, he named the suite of scripts 『Personal Home Page Tools,』 more frequently referenced as 『PHP Tools.』 」 [1] PHP is a marvel of how a horrible language can become the foundation of large numbers of applications… for a second time! Worse is Better redux. According one informal but interesting survey, PHP is now the 4th most popular programming language out there, losing only to C, Java and C++.
  • JavaScript, by Brendan Eich circa 1995, 「Plus, I had to be done in ten days or something worse than JS would have happened.」 [2] According to that same survey, JavaScript is the 5th most popular language, and I suspect it is climbing up that rank really fast. It may be #1 by now.
  • Python, by Guido van Rossum circa 1990, 「I was looking for a 『hobby』 programming project that would keep me occupied during the week around Christmas.」 [3] Python comes at #6, and its strong adoption by scientific computing communities is well know.
  • Ruby, by Yukihiro 「Matz」 Matsumoto circa 1994, 「I wanted a scripting language that was more powerful than Perl, and more object-oriented than Python. That』s why I decided to design my own language.」 [4] At #10 in that survey.
說實話……比王垠牛逼的人太多了……真正搞程序語言的圈子根本沒人知道誰是王垠……他的東西很多都是別人早搞好了的……程序語言的圈子非常小眾，大牛就那幾個，國內搞的更少。這個方向最牛的華人是耶魯計算機系主任邵忠（科大少年班畢業）。國內能拿得出手的也就清北科了。等你花個三五年時間，能讀懂POPL，能發個程序語言方面PLDI、OOSPLA，回過頭來你就發現王垠搞的就是自娛自樂的玩具。當然他很牛，就壞事在他孩子一樣的脾氣上……如果他能踏實一些，也許會多一個大師。

玄學
祈禱自己寫的編譯器（解釋器）不出神bug

偏系統方面的話，是編程語言種種技術在軟體系統中的種種應用，顯然是搞PLT的數學家們所不齒的。一般大家如果聲稱自己是研究編譯器的話通常就是搞這類應用了。搞應用的話主要思路是和熱門方向接軌，為炒的沸沸揚揚的上層應用提供一個更快、更並行、更可拓展、更穩定、更安全、更節能的編程環境和程序運行環境，讓程序員們能更歡樂地編程。這類研究一般需要上層應用、中層虛擬機和底層操作系統的兩兩配合，程序分析的根基又在於編程語言理論，簡直是巧妙地融合了理論、系統和應用啊。還有研究面向某一種特別架構的編譯或內存管理技術以達到同樣目的的，譬如專門針對CPU+GPU環境的，或者針對嵌入式系統，或者針對Non-volatile內存系統。會議的話，與ICFP之類的就毫無瓜葛了，基本是從PLDI一路投到OSDI：

大而廣的、如雷貫耳的：PLDI、OOPSLA，大家最拿得出手的才往這裡面投
SIGARCH，SIGOPS，SIGPLAN聯合出品的專門搞PL和OS交叉的：ASPLOS - Architectural Support for Programming Languages and Operating Systems
次一檔的：ECOOP、CGO、ISMM
專註於虛擬機的：VEE - ACM SIGPLAN/SIGOPS International Conference on Virtual Execution Environments （據我導師說這兩年開始偏系統虛擬機而不是JVM這樣的進程虛擬機）
面向系統架構的（小會）：
LCTES - Languages, Compilers, and Tools for Embedded Systems
CASES - Compilers, Architecture, and Synthesis for Embedded Systems
面向並行環境的：
PPoPP- ACM SIGPLAN Symposium on Principles and Practice of Parallel Programming
LCPC - Languages and Compilers for Parallel Computing
偏軟體工程的：
ICSE - the International Conference on Software Engineering
FSE - International Symposium on the Foundations of Software Engineering
然後操作系統的一些會議也或許能投：
SOSP - The ACM Symposium on Operating Systems Principles
USENIX ATC - USENIX Annual Technical Conference
OSDI - USENIX Symposium on Operating Systems Design and Implementation
如果搞的是Haskell之類的Runtime的話ICFP之類的也能投，譬如GC的早期技術，畢竟自動GC最先出現於Lisp的實現。

再貼幾個我們這個領域的幾個目前活躍的有代表性的美國的研究者的研究方向，最具代表性的之一肯定就是

Vikram S. Adve
Deterministic-by-Default Parallel Programming
SVA: Secure Virtual Architecture
SAFECode: Static Analysis For safe Execution of Code
LLVM Infrastructure
LLVM當時其實並不是他的項目之一，但他依然慷慨支持了Chris Lattner寫LLVM。現在又搞了許多LLVM的衍生項目。

Home page of Michael D. Bond
Program analyses and software systems that make complex, concurrent software significantly more reliable, scalable, and secure than it is today.
這貨和另一個澳洲國立大學的Steve Blackburn（在下面）教授是Jikes RVM的主要貢獻者。

Emery Berger
這個人研究GC研究的很多，他跟Mike Bond同是Kathryn S McKinley 門下的。他有個比較有名的作品是根據今年教授的活躍程度對學校進行排序，網站叫csranking，比US News排名更有參考價值。

Steve Blackburn
Microarchitectural support for managed languages, fast and efficient garbage collection, and the design and implementation of virtual machines
除了Jikes，Java的DaCapo Benchmark也是他和Kathryn S McKinley搞的。

Home Page of Professor Michael Franz, University of California, Irvine
Compiler, virtual machine, and related system-level techniques for making software either safer, or faster, or both. Some of this research also falls under the labels Computer Security, Trustworthy Computing, and Software Engineering.
這兩年剛評上ACM Fellow，HotSpot Client編譯器的主要作者之一Christian Wimmer去他兒做過一會兒博後。他們系還有一個年輕的華人AP Harry Xu，也很活躍，研究方向類似，近年灌了不少PLDI，OOPSLA。

--------------------------

王垠在PL方面肯定還是很有料的，至於他的言論，他總喜歡用他的那一套 「設計者的眼光」 去看待一切事情，有時候一驚一乍，有時候故作清高，有時候把自家的狗牽出來說是只老虎，然後最後又說自己顯然在扯淡，總體還是十分可愛的。同樣我們作為讀者，也應該用 「撰寫者的眼光」 去閱讀他的文章，這樣你就只能知道他到底哪部分嚴肅哪部分扯淡了。

無責任瞎猜：類型系統、數學理論、其它……

這個問題好難啊。

就中科院系統而言，相關方向的團隊全部列出來如下：
中科院軟體所計算機科學國家重點實驗室
中科院計算所計算機體系結構國家重點實驗室-編譯與編程實驗室
中科院信工所第六研究室

因為這一方向入門門檻較高，所以上述團隊都不是特別大，招生也不多。

formal verification, program synthesis, analysis etc.
http://www.cs.colorado.edu/~bec/

哲學和AGI。其餘屬沒入門的，並且基本都是永遠入不了門的類型，呵呵

實際上是：有語言研究，沒有編程語言研究。

推薦閱讀：

※男朋友在研究所工作，買一台SONY DPT-RP1 方便看文獻做筆記嗎？科研人員有推薦嗎？
※有些中文論文好垃圾……怎麼能把它們過濾掉？
※研之成理是由誰建立的？這是一個怎樣的團隊？
※如何研讀一篇論文？
※工科研究生使用macbook pro合適嗎？

TAG:編程語言 | 科研 | Scheme | 可計算性理論 |