北大十年，博士畢業(yè)后，他去了華為。

那時我本科畢業(yè)已然多年，但仍舊清晰地記得，當年每當期末考完一科后的夜晚，側(cè)耳傾聽四鄰宿舍或沉默或欣喜，抑或是開黑傳來的吵鬧，這種感慨都會在心頭徘徊。而我自己，在這人間百態(tài)里只能一邊盡力跟上課程，一邊尋求自己喜歡的科研方向。

在或深夜或凌晨昏暗的路燈下，我早已經(jīng)不記得在“麥教”度過了多少個通宵的夜晚。在努力掙扎與不斷被虐的交替中，時光就這樣匆匆流過。從本科到碩士，再到轉(zhuǎn)成碩博連讀，我跟著當年還是副教授的孫猛老師踏上了形式化方法研究的道路。

形式化方法旨在通過數(shù)學模型，為計算機軟件或硬件系統(tǒng)進行精確的描述，并通過數(shù)學方法證明其可靠性，消除系統(tǒng)中潛在的錯誤。所以，這個方向的研究既需要相應(yīng)的數(shù)學功底，也需要對計算機領(lǐng)域有較深的理解。換言之，需要大量的背景知識來支撐科研的進行。還記得剛開始讀研的時候，我同時參加自己師門的討論班、系里的大組討論班和中科院軟件所的討論班，最多的時候每個月要分享兩次，每次兩個小時?，F(xiàn)在雖然看起來不難，但對于那時的我來說，通讀一篇論文準備兩個小時的PPT幾乎要花費一周的時間。除研究生課程之外，讀論文、討論班分享幾乎占據(jù)了生活的絕大部分。

憑借著興趣的支撐，我終于慢慢從科研菜鳥，熬成了有自己想法，有明確目標，想要做一些“有意思的事”的科研熟手。也就在這個時候，認識的師兄師姐漸漸開始就業(yè)，自然地，我也會偶爾把目光投向他們——等我畢業(yè)之后，應(yīng)該何去何從？然而隨著對就業(yè)市場的了解不斷積累，殘酷的現(xiàn)實開始慢慢浮出水面。

形式化證明研究是為了提高軟件質(zhì)量，并力圖實現(xiàn)極致的系統(tǒng)可靠性而存在的，可以說與計算機軟件的歷史相伴而生，歷史上不少大名鼎鼎的研究者如圖靈都是形式化方法的研究者，但這一研究現(xiàn)在多用于航空航天、列車控制等領(lǐng)域。為做出極致可靠的系統(tǒng)，需投入大量的人力物力財力，這對大部分公司并不是最佳選擇，也因此我們的就業(yè)方向基本以學校和科研院所為主。目所能及，除了做博士后走教職這條路之外，那幾年我看到就業(yè)的師兄師姐們幾乎都選擇了改行。

說來也許很多人都不會想到，在北大博士的光鮮外表之下，我曾經(jīng)做好了畢業(yè)即失業(yè)的心理準備。雖然繼續(xù)搞理論科研確實是一條道路，但是打從心底里，我仍然希望能夠?qū)W以致用，我想要做一些真正在實踐中就能用得上的東西。

在這個時候，華為來到了我的生活?；蛘哒f，我的生活里走進了華為。

2018年4月，在春暖花開的時節(jié)，在象牙塔中度過了近九年的我，也終于不可避免地走上了糾結(jié)的求職路。在征得導師的同意之后，我向包括一眾互聯(lián)網(wǎng)大企業(yè)在內(nèi)的公司投出了簡歷。我的要求不高，只希望能夠找到一個專業(yè)對口的崗位，不浪費這些年的學習與科研經(jīng)歷，但是要么石沉大海，要么“查無此崗”，一些比較友好的HR還會主動向我推薦人工智能類算法崗位，理由是“這樣不浪費你的博士學位”。在驚異于人工智能就業(yè)市場如此火爆的同時，除了感慨自己方向之冷門，實在也無法可想，無計可施。這樣一個多月下來，基本沒有什么實質(zhì)性進展。

直到偶然的一個機會，在一個微信群里，我看到了來自華為中軟的招聘宣發(fā)，意外的是，在其中看到了“形式化證明工程師”的崗位。機會很是難得，雖然之前對華為的了解并不多，但是試試總歸沒有壞處。抱著這樣的心態(tài)，我甚至都沒有特地準備單獨的一版簡歷，把之前用的中英文簡歷直接投到了招聘郵箱。

其實對于華為有這個方向的招聘需求，老實說有點出乎我的預料。那時華為的軟件產(chǎn)品由于目標客戶群等原因在高校曝光率極低，在周圍同學的主流認知中，華為是一家“硬件公司”多于“軟件公司”。而形式化證明介于軟件理論與軟件工程之間，很難想象一家“硬件公司”會存在這方面的需求。但更加意外的是，不到半個小時，來自華為OS內(nèi)核實驗室的電話就打了進來。沒等我過多介紹自己的具體工作，對方就開始滔滔不絕地講起了部門在這個方向上的宏大計劃……

電話打完沒多久，部門就安排了實習面試。效率之高讓我著實又驚訝了一把。一周之后，我就掛上實習工卡，站在了北京華為大廈的門口。

每周一、三、五在公司實習，周二、周四則回學校繼續(xù)搞科研，改論文，還要應(yīng)付畢業(yè)前夕需要準備的各種材料，畢業(yè)論文初稿、預答辯等事宜，實習期間的生活不可謂不辛苦。但是終于有機會走進真實的工業(yè)場景，這又令我相當振奮。OS內(nèi)核實驗室負責公司自研操作系統(tǒng)內(nèi)核的開發(fā)，操作系統(tǒng)內(nèi)核是系統(tǒng)軟件中的核心部分，即便是一個微小的錯誤也可以引發(fā)嚴重的后果。因此同事們在開發(fā)過程中十分謹慎，在這種近距離感受工業(yè)開發(fā)的場景中，我了解到許多從前在學校中從未接觸的問題和挑戰(zhàn)。

在學術(shù)的世界里，我們往往做好了很多假設(shè)，將一個問題抽象到相當?shù)母叨?，一如物理學家計算出“真空中的球形雞”一樣，這樣的抽象有利于我們更好地集中觀察并解決特定的問題，然而在現(xiàn)實業(yè)務(wù)中，性能、安全、效率、交付……都制約著這種抽象的可能。客戶認可你對問題的簡化嗎？同事認可你在簡化問題下拿出的“完美”方案嗎？答案顯而易見。在這種場景下，我們必須拿出更加貼近實際，在各種工程困難下仍然保證軟件可靠性的解決方案。在這樣艱巨的挑戰(zhàn)之下，我在團隊其他同事的帶領(lǐng)下，嘗試了不同的方向，進行了大量的調(diào)研，打算自研軟件形式化證明工具。

在這種務(wù)實的氛圍之下，我也慢慢適應(yīng)了華為快節(jié)奏的生活。從最開始的一周三天，到后來提交畢業(yè)論文之后每周全勤，最初預想的“入職前休息一月去畢業(yè)旅行”，最終變成一畢業(yè)就完全投入到研究工作中來。

這時2019年已過半載，美國實體清單的風波之下，周圍同事們壓力倍增。為了節(jié)省通勤路上的時間，能夠每天多做一點事情，我抽時間去駕校考了增駕，然后買來了一輛摩托車。引擎的震顫伴隨著激昂的心緒，大概是那個時候心情最好的注腳。

2019年8月，我提著行李箱走出深圳寶安國際機場，來到了東莞松山湖溪流背坡村。

為了完成終端的“補洞”目標，松湖會戰(zhàn)在這個炎熱的夏日拉開了序幕。在公司的召集之下，我推遲了新員工培訓計劃，直接在東莞辦理了入職手續(xù)，并在松山湖畔開始正式工作。

松湖會戰(zhàn)中，每個參與團隊均由國內(nèi)員工和數(shù)量不等的海外研究所的本地員工參與，雙方在同一個課題上展開合作攻關(guān)。在北京習慣了快節(jié)奏生活的我，在與海外研究所同事的合作中又重新“慢”了下來。但是這并非是銳氣的消弭，而是工作節(jié)奏的進一步沉淀。

“This might work for now, but it is not the way expected.” （這可能暫時可行，但這并不是我們所預期的方式。）

外籍同事做事長于細節(jié)，凡事不求速成，而是要從頭開始，自己琢磨。對同樣的工作，他們很多時候上手速度慢一些，但是一旦進入狀態(tài)，他們對于技術(shù)細節(jié)的掌握要更加準確。很多時候我們面對一個問題，一旦找到可供參考的解決方案，第一反應(yīng)就是去做一個簡單的實驗來驗證方案的可靠性，有了最初的結(jié)果后就開始往下推演。而外籍同事們往往要先把論文吃透，代碼行為逐行搞個一清二楚，很多時候還會自己從頭實現(xiàn)一遍，踩一下其中可能存在的坑。這種方式自然會消耗大量的時間，但是最終的解決方案很多時候確實也有著更高的可靠性。因此到底應(yīng)該“have a demo for now”（先做一個demo），抑或是“make it the way we expected”（按我們預想的方式）就成為了我們思維方式碰撞的焦點。

我們的項目中有一部分工作需要對源代碼和一種中間表示進行人工核對。這是一個相當繁瑣的工作，而且需要核對者本身對代碼和中間表示都有相當?shù)牧私狻Ｍ饧翯erman接手了一部分核對工作，結(jié)果——沒過幾天，我就在他的電腦屏幕上看到了一套外文版的《編譯原理》。

“這也行？這書看一遍怕是幾個星期打不住。”我心里對進度能否趕上頗有疑問，但好在這項工作我們共同完成，開始的一段時間我可以多趕一點進度來讓German熟悉相關(guān)知識。果不其然，最開始的一兩個星期他幾乎沒有任何輸出，但隨即而來的就是，每個星期他在核對中發(fā)現(xiàn)的問題都是最多最細的，幫助我們修復了很多潛在的bug。

“如果一座樓的地基深度只夠建造5層樓，那么當我們需要把樓高加到10層的時候，就不得不在旁邊重建一座新樓。但是如果新樓的地基只夠建造10層，那么可以想象，接下來旁邊又會有第三座、第四座新樓……”每當與人討論軟件質(zhì)量的時候，我都會打這個比方?，F(xiàn)實中應(yīng)該不會有房地產(chǎn)開發(fā)商向設(shè)計師提出這種需求變更，但是客戶對軟件的需求卻實實在在存在這種可能。這時候，外籍同事們從一開始便對每一個細節(jié)仔細琢磨，并考慮這種做法是不是“優(yōu)雅地”合乎程序的設(shè)計美感的做法，初看雖有失性價比，但是長遠考量確實有很大的潛在收益。然而目光長遠，精雕細琢一定是好的嗎？我們也已經(jīng)有了許多例子證明：并不是。經(jīng)歷了長時間的雕琢之后最終證實一項功能無法實現(xiàn)，或者最終不符合我們的需求，這種例子在工作中可以說比比皆是。

2020年1月，連地處嶺南的東莞也漸漸冷了起來，不知不覺間我入職已近半年。在這半年里，我們自主開發(fā)的形式化證明工具已頗具完成度，成功發(fā)現(xiàn)了系統(tǒng)中的一些缺陷，產(chǎn)生了真正的商業(yè)價值。作為一名新員工，在這半年里，我和同事們經(jīng)歷了求同存異的思想碰撞，共同工作中精益求精，砥礪奮進，我感受到了不同民族文化、性格與思維方式的差異，更親眼看到、親身體驗了華為人的精神與華為的文化。

做好每一件事的細枝末節(jié)，追求端到端、點到點百分之百的可靠，這種執(zhí)著是科研人的本分，也是業(yè)務(wù)核心競爭力的重要組成部分，如同在下班路上目睹的寧靜幽美的松山湖畔夜色，平穩(wěn)而不浮躁。與此同時，作為一個在商海之中沉浮的“巨無霸”公司，又必須具備敏銳的嗅覺，在戰(zhàn)場上銳意進取，奮勇直前，即使是預研類業(yè)務(wù)，也絲毫不能懈怠。我無比熱烈地尋求每一個可能的應(yīng)用場景與機遇，期冀實現(xiàn)個人與公司的發(fā)展，一如在摩托車上所看到的北京——轟鳴的引擎聲中，通明的燈光與人流的喧囂一閃而過，這是超級都市的節(jié)奏與心跳，也是我們必須要適應(yīng)的生活。

華為的核心價值觀，落實在業(yè)務(wù)的角度上是“以客戶為中心”，落實在人的角度上是“以奮斗者為本”。什么是奮斗？什么是奮斗者？想來十八萬同事的心中，自有十八萬種不同的定義。在我看來，松山湖畔溪流背坡村的東莞夜色和摩托車上呼嘯的北京，這兩種不同的生活和工作模式，看似對立，實則統(tǒng)一。它們共同構(gòu)成了我豐富多彩的生活，也共同鑄就了我心中對于奮斗的定義——“在奮勇直前的道路上努力做到精益求精，并一以貫之直到旅途的終點”。

這是我對過往的總結(jié)，也是我對未來的希冀。人生苦短，勉之勉之。