Common Lisper

本文简要介绍我于2024年2月25日（农历正月十六）至3月5日 “秘密” 回国期间的主要经过。必须声明，之所以没有事先在微博上公开宣传，绝不是怕广大网友知道，而是还有别人（主要是我妈）可能也盯着我的微博。我回国的消息一旦泄露就有可能给我在老家期间的生活带来不必要的麻烦。

还是得回忆一下。我上一次回国是2020年的1月20日（春节前夕），当时预期两周内返回意大利。但随后 COVID 疫情爆发，从武汉迅速蔓延到全国乃至全世界，我就被迫滞留在国内直到当年的10月19日才得以返回意大利继续读博。后来我就不敢再贸然旅行了，专心读博直到2022年11月23日顺利拿到博士学位。然后一边在 FBK 原地做博后（短期合同，经历了多次延期），一边配合澳国立大学（以下简称 ANU）给我办签证。5月底我在FBK的合同结束（我实在受不了写Python的工作，主动要求不再续签了，然后每天专心继续学梵语）。虽然我是破釜沉舟（一旦耗尽资金就可能连去澳洲的机票都买不到，但幸好7月份签证就到了，我花光自己几乎全部的钱才顺利迁居澳洲。（我可能是ANU历史上招募周期最长的员工，从我拿到offer到最终报到，超过了一年。）总之我已经四年没回家了。

我滞留国内期间包括在杭州生活的几个月。之所以去杭州是为了三件事：1. 跟我前妻办理离婚手续。2. 户口迁回辽宁以后依法我可以提取在杭州工作期间的住房公积金（大约20万）。3. 我的意大利居留在滞留期间过期了，要回去就必须重新办签证。最终只有第二件事办成了，在立刻给我爸汇了5万以后，剩下的钱就是我买新电脑（2019 MBP），给同住在青旅的绿头发小姑娘买电脑（MBA）、借她1万块钱等，以及我自己在杭州生活几个月的资金来源。第一件事实际不需要办，我前妻骗了我，她在跟我约好同去民政局的当天早上才微信告诉我手续早就离完了，具体方法是她在2018年我完全不知情的情况下单方面去法院起诉离婚，她说我“结婚不到俩月就突然人间蒸发”所以要求离婚。法官也不知道我出国留学了所以直接就给判了（法官同志就往我原单位打了个电话，但是接电话的同事以为我犯什么事儿了，出于好心决定一问三不知。）总之我去法院顺利拿到了离婚判决书复印件（这份文件后来在我办理澳洲签证所需的婚姻状况证明时效力等同于离婚证）。至于留学签证，我去了上海以后才发现原来我户口迁移后的领区变了，必须去北京（沈阳的意大利领馆在疫情期间关闭了），虽然历经周折但并没有什么本质上的困难。只能说我人生坎坷，遇人不淑，以及疫情背景下我的博士学位来之不易。

最终，我顺利持永居签证（PR）从意大利迁居澳大利亚，成为了澳国立大学 (ANU) 的一名普普通通的博士后（3年合同）。算起来，我并没有丰富的论文发表成果，跟ANU 的同事（甚至包括一些在读博士）相比，我的名片还太差了，平时最好低着头走路。我也几乎没有什么人脉，更没有什么积蓄（从 FBK 离职后在意大利累积的养老金刚好够买去澳洲的机票），跟两位博导的关系仅限于表面和谐（跟硕导的关系倒还不错）。这份博后工作完全是我自 2017 年以来在定理证明领域用数万行代码跟未来导师堆出来的，跟我在博士期间的研究工作无关，而且我日后也不打算再跟两位博导合作发表论文。

我现在终于过上了曾经梦寐以求的生活：每天只做自己喜欢的事情——无论科研工作还是日常生活都是。工作上除了一点点大学日常琐碎的事务以外我只专心把形式化证明写好（目前研究的是 λ 演算相关的一些高阶理论）；生活上，自从租到了不错的房子以后我就开始在后院种菜（和葡萄），目前各种植株都涨势喜人。我在数学（主要是概率论相关）和数学形式化方面的知识储备，目前来看在学院里还是拿得出手的，经过一次本校的夏令营，系里的同事在数学方面已经不敢再小瞧我了。我对梵语的爱好和计算机相关研究计划也已经跟导师确认过可行性，只等完成了半数的现有工作计划以后我就可以自行开展了。

自从8月最后几天到达澳洲以来，四个多月过去了。距离我通过大学的工作试用期还有两个月，虽然不太可能发生意外但也马虎不得。我在本地没有结交一个新朋友，跟中国室友们的关系也仅限熟人。我刻意消除了一些社交活动，最小化地与人交往，平时除了工作和购物以外绝不出门（拍照仅限于家附近）。最重要的是，我平时见美女低头绕着走（丑女就更不用说了），以免被骗婚；跟本校的女学生绝不打任何交道（以免犯那种导致被开除的严重错误）。社交最小化的原则我打算一直保持下去，直到有了重大学术成果，工作彻底稳定为止。所谓 “终身大事” 要是跟生存本身相比，也就不算事儿了……

我现在最重要的事情就是不能把一手好牌打个稀烂。如果顺利的话，澳洲可能就是我的职业生涯的终点：我要努力工作，一点一滴地积累自己的学术成果（以及未来的养老金）。但另一方面，我没有所谓的 “定居” 或者移民（即拿澳洲国籍）计划。我也不贪图国外的生活，无非是躲个清净罢了。由于我的科研工作既不需要特别强大的电脑，也不需要其他什么昂贵的科学仪器。只要中科院高薪聘请，我愿意随时回国工作。（无非是跟现在的导师恢复过去的远程合作模式罢了，影响不大） 

PDF download.

下面简短地写个年鉴。

我的 2019 年总体来说是成功的。自从拿到新的学生签证、带着《梵语入门》返回意大利以后，我就正式开始了博士第一年的学习和研究。我发表了两篇跟自己专业相关的会议论文 [1,2]，然后靠着它们通过了博士第一年底的升学资格考试。我的硕士毕业项目当初留下了一点儿遗憾，我后来继续改进，又写了5000多行代码，跟硕导 D. Sangiorgi 合写出一篇期刊论文，不过目前尚未最终发表。此外，我还给 HOL4 定理证明器提交了大量概率论形式化方面的代码改进，在形式化证明 “强大数定律” 的道路上又前进了一大步。另一方面，我的梵语学习达到了过去七八年来的最佳水平，不但掌握了大量的词汇和例句，而且在梵语计算语言学（古代语法规则的计算机模拟）方面也有进展——找到了同行的大量研究论文，看后豁然开朗。其他语言方面，在古希腊语和古希伯来语上略有进展，尤其是总算记住希伯来文的元音加点规则了。

跟导师 A. Cimatti 的关系搞的不太好，尤其是在他得知我跟硕导合作发表期刊论文的事情以后严厉指责我背着他搞其他学术活动。他的心情我可以理解，但是我在有了新的学术贡献（不论多小）以后也有责任将它们发表出来，让后续的研究者少走些弯路也是好的。何况这篇期刊论文还可以作为博士毕业要求的两篇论文之一，极大减轻了我的毕业压力。总之虽然他认可我的能力和取得的成绩，并且让我正常升学了，但可以看出此人有极强的控制欲，甚至还有一些嫉妒心。我强烈怀疑他的学术能力十分有限，过往的声誉主要是通过论文作者姓氏比划排序得到的。我得到的有效学术指导很少，2019 年里可以说几乎没有，甚至是负面的。我不确定自己能不能在意大利顺利完成三年的博士学习，今年之内被迫结束学习然后回国重新换个国家重新申请博士也不是不可能。我现在唯一的希望就是努力发表论文（包括违背导师意愿发表我自己的论文），以我所属大学的利益为先，确保我导师找不到冠冕堂皇的理由提前结束我在意大利的博士生涯。

生活方面，由于我平时精力主要放在学习和科研上，并且尚未离婚，虽然结识了少数异性朋友，但都没有什么深交。我也有意避免跟异性过多接触。平时最多的娱乐是上网看看电视剧以及打打游戏（比如在 switch 上玩《巫师3》）。岁月蹉跎，我如今已经 38 岁，很快就算中年人了，就连当初比我小8岁的跆拳道小姑娘都已经虚岁30，结婚好几年了。而我还在博士的道路上苦苦挣扎，前途乌云密布。可能唯一的欣慰就是，作为一个博士生，身处意大利，周围的一切研究都相对 trivial，我的学术压力很小；偏理论的研究方向也不需要除笔记本电脑以外的任何实验设备，从来没有卡在研究工作上。这个博士学位的唯一用途，可能就是让我能以博后的身份再在国外呆几年，享受学习的乐趣。另一方面，我在博士第三年里计划回杭州（母校浙江大学）交流访问半年（至少三个月），顺便找律师办离婚。这个计划能否顺利实施，主要看我导师能不能让我进入博士第三年，今年10月底见分晓。不管怎么说，活下来就是奇迹。我现在所花的每一分钱都来自博士奖学金：他们付给我钱让我做一些自己也感兴趣的事情，同时我还有大把时间学习自己感兴趣的其他东西，就算随时中止这种生活，我也算是赚到了。

下面简要介绍一下我从1月8日到2月5日间秘密回国的背景，以及在杭州生活了近一个月的主要经历。

事情的起因是这样的：意大利法律很奇葩地规定外国人的居留许可（Stay permit，以下简称 “居留”）只能从学习转换成工作类型（这样毕业后可以直接找工作），反方向则不行。如果曾经在意大利工作，持有工作居留，身份变回学生以后必须回祖国重新办理留学签证，然后再回到意大利申请新的学生居留。我在 FBK 的一年工作期间已经把自己的居留许可转成了工作类型，2019年2月16日到期。我必须找个适当的时间回国重办留学签证。如果因为某种原因不能得到签证，那我也要争取在现有居留过期前返回意大利一次，亲自料理彻底回国前的各种后事。另一方面，我的旧护照将在2019年3月3日过期，为了确保新的签证贴在我的新护照上（从而确保我在拿到新的居留之前——需要等2到8个月——可以自由前往其他申根区国家），我必须先更新护照。所以我在去年10月底就开始申请换发护照，并于2018年11月30日拿到新的护照，然后就立即开始筹备回国所需的各种文件和资金，最后在1月7日出发，1月8日上午到达了杭州。之所以去杭州是因为我还有其他事要办，比如过期的身份证，先前以为必须去上海办签证，但后来发现意大利在上海的领事馆在杭州也有签证中心，所以我直接飞到了杭州并一直住在那里。

其实根据意大利法律，我在2017年12月从博洛尼亚大学硕士毕业之后的一年里，虽然已经不是学生，但在2018年2月的时候是有资格再更新一次学生居留的。这是意大利政府留给外国留学生毕业后在意大利找工作用的窗口时间：如果一个外国学生在意毕业一年内找到工作了，那么接下来就可以转换成工作居留，今后只要继续合法工作就可以一直生活在意大利。毕业后的这次续居留的各项条件跟之前续学生居留的手续是一样的，但我却无法操作，因为我毕业后身上已经没什么钱了，无法提供 5500 欧元的资金证明（其实可以临时跟别人借一下，但这对我来说这已经不算是合法行为了）。但我是有正式工作和工资的，医疗保险和养老金也是 FBK 支付的，所以只能转换成工作居留。代价就是当我正式开始读博士以后，必须回国重办留学签证。所以我为了这次回国的已经筹备了整整一年，为了确保不出现意外，不被人使坏，我没有在任何场合公开透露过相关计划，所有关键时间点完全保密，回国期间也保持低调，仅在需要帮助的时候联系了最可靠的朋友，甚至我在杭州的住宿地点也碰巧因为试营业暂时没有在公安局备案，只要我不说就没有人知道我住在哪里。在我顺利拿到新的意大利签证并且返回意大利之前，我要防的不仅是我的准前妻，而是所有的人，只有极少数值得信任同时没有利益冲突的（女性）朋友除外。

2018 年是我硕士毕业后逐步转变成严肃的科研工作者的重要一年。整整一年里我在 位于意大利北部特伦托 (Trento) 的 Fondazione Bruno Kessler (FBK, 意大利顶级科研机构) 里工作，在未来博士导师的指导下从事严肃的科研工作。一年来成绩还是不错的，我在自己的主攻方向——Runtime Verification——上取得了一些新成果，这些内容极大地充实了 FBK 在欧盟 CITADEL 项目里的贡献度。但可惜从4月份开始跟两位领导一起撰写的会议论文，7月的时候被拒稿了。不过相关的发现是实实在在的，几千行代码是同行无法轻易复制的，只能希望接下来的投稿不要再被拒了。

另一方面，没想到我去年的毕业项目还有潜力可挖。我的硕士毕业导师 (Davide Sangiorgi) 在6月份突然联系我，建议将我毕设的精华部分抽出来合写一篇 workshop 论文，投给9月份在北京召开的 CONCUR 2018 会议下面的 workshop。我抱着趁机可以回国和回家看看的想法同意了，结果这篇草草写就的论文竟然被接受了，成为了我硕士毕业后的第一篇公开论文。后来11月份的时候我们还受邀再写一篇完整版投给某期刊，目前这篇论文尚未完成。其实这些研究工作倒也算不上惊天地、泣鬼神的重大领域，但作为我博士生涯开端时期的练手项目还是合适的。即便论文成功发表，我心中也并不是十分喜悦，因为毕竟是很小的工作。也许唯一的用处就是让我自己的导师惊讶一下，以免他平时太小看我了。

除此之外，我在概率论（和测度论），图论和 Runtime Verification 的 HOL 形式化方面也有一些成果。其中在概率论形式化方面，我发现目前 HOL4 里官方自带的形式理论跟现代教科书里的版本还有很大差距，基础定义存在各种问题，上层建筑也很缺乏，几乎无法使用。我在博洛尼亚大学期间花费了许多时间学习概率论和随机过程，我一直希望能把（强）大数定律完整地形式化出来，为了这个目标，我从8月份开始着手改进HOL4的概率论形式化代码，工作量十分巨大，但好在其他人已经打下了基础。这个工作我从夏天干到秋天，从圣诞节干到中国春节，直到目前还没干完。我在这些个人研究上花费了大量时间，但写出的论文将是属于我自己的，代码则会长久地留存后世，所以很值得。

2018年是我历史上写代码写得最多的一年。工作直接相关的代码（C/C++）写了上万行（而且反复改动过），HOL 形式化代码（Standard ML）也写了一万行。其他还有 Common Lisp 开源项目的代码，Adobe Acrobat Pro 插件 (C++) 和自定义动作 (JavaScript) 的代码等。很多过去多年来我想学但是没学会的东西（包括 CORBA 和 ANTLR 的 C++ 接口）今年终于基本学会了。自从学会了自定义 Acrobat Pro 以后我的 PDF（批量）处理技术日益提高，还花钱把 Acrobat 2015 升级到 Acrobat 2017。年底的时候还重学了点儿 MFC 和 Win32 编程，不过因为并不急用所以并没有坚持下来。

自然语言方面，年初我在 FBK 参加了初级德语课程，完成后拿到了相当于 A1 的证书。此外我还学了一些圣经希腊语和希伯来语，并买到了当今最好的教材（有配套视频教程）。我在梵语方面一直也没有停下来，今年里我几乎每天上下班时都带着以前的旧梵语课本，在上下班的火车上背诵各种语法表格，终于把最基本的动词变位表给背下来了。梵语的《帕尼尼经》我在今年里也有所领悟，过去几乎一点儿都看不懂，现在已经好多了，可以跟现代的语法书联系在一起了。其他小语种（法语和拉丁语）我也稍微复习了以下，尽量维持过去的知识水平以便将来再提高。至于意大利语本身，无论对话还是阅读我现在都已经相当不错了，词汇还是欠缺，但只要有机会就去上课继续巩固。

我这次的博士录取没有发生什么意外，因为一方面导师确实对我的工作很满意，另一方面我的硕士毕业成绩也很不错，自然排名就很靠前。特伦托大学比较富裕，每年计算机相关领域博士招生数额是博洛尼亚大学的5倍以上，所以7月份的时候我顺利收到特伦托大学正式的录取信，然后11月份正式开始了博士生涯。奖学金每年1万6千多欧元够花了，不过比我之前在FBK工作期间的工资略少一些。这些都是导师事先都讲明了的，所以也没什么可计较的。这些钱保证我一个人未来三年在意大利的正常生活是足够了，还可以少量地补充些软件和硬件。种种留学相关手续十分麻烦，但我是合法身份，所以虽然花费了不少时间但并没有遇到任何实际困难。

6月份的时候用闲钱买了个任天堂 Switch，然后断断续续玩了几个月的《塞尔达传说》。其实我平时最主要的休闲就是联网跟几个欧洲玩家几乎每晚一起打 Navalogic 的老游戏《Joint operations》的自定义任务。每天看书、写代码、打游戏，基本上也就没有时间再干别的了。我以前在意大利看到漂亮姑娘还在心里掂量值不值得出个轨什么的，现在我连看都不看了，专心把自己的科研工作做好、早日拿到博士学位才是正道。意大利最不缺的就是帅哥美女，这个国家缺少的是有责任心、肯吃苦耐劳的高科技人才——比如说敝人。所以我准备暂时留在这个国家，致力于让意大利跻身欧洲计算机科学研究的前列。

关于我的博士生涯，目前的计划是争取三年内准时毕业，这就意味着两年半之内必须完成博士论文——目前课题我已经基本想好了——然后最后半年一边交换学习一边等博士论文评审结果。时间已经不多了，不过好在我在 FBK 工作的一年相当于已经读完了博士第一年了。我准备把 Monadic Second(-Order) Logic (MSO) 和 Runtime Verification 结合起来，把我所有的知识都用上，写一篇前人想都不敢想的博士论文，快速毕业然后开始拿博士后的工资。

其他没什么可说的了。