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

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

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

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

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

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

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

在這個(gè)時(shí)候，華為來到了我的生活?；蛘哒f，我的生活里走進(jìn)了華為。

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

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

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

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

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

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

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

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

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

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

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

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

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

我們的項(xiàng)目中有一部分工作需要對源代碼和一種中間表示進(jìn)行人工核對。這是一個(gè)相當(dāng)繁瑣的工作，而且需要核對者本身對代碼和中間表示都有相當(dāng)?shù)牧私?。外籍同事German接手了一部分核對工作，結(jié)果——沒過幾天，我就在他的電腦屏幕上看到了一套外文版的《編譯原理》。

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

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

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

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

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

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