Chun Tian (binghe)

人生就要丰富多彩，不断的变化中谋求暂时的稳定和内心的安宁。其他诸如事业、金钱、女人什么的都是次要的，对这些东西的追求从来不是人生目标本身，只是作对了其他事情以后自然获得的奖励罢了。

2017 年是我在意大利留学（攻读硕士学位 ）的收尾。事实上直到这一年的到来我都还活在过去的工作状态里，在相对富裕的生活状态中享受着学习的乐趣。自从 2016 年 10 月失业以后，生活一度陷入危机，然后我不得不收回过去的借款和寄给我父亲的钱以维持我毕业前的生活。所以我开始省吃俭用，同时一步一个脚印地完成毕业所需的剩下的考试（2017 年里通过了最后五门考试），以及毕业项目。

2017 年也是我开始掌握定理证明技术和逐步确定毕业项目的一年，事实上直到 2017 元旦以前我连一个定理也证明不了，可是元旦

经过三年多的努力，我终于以满分 (110L) 的成绩从意大利博洛尼亚大学毕业（毕业项目和论文），拿到计算机科学硕士学位。从此再从事计算机相关工作终于算是科班出身了。

我十多年来最大的心愿是学会定理证明技术，最后如愿以偿，毕业项目就是用定理证明器 (HOL4) 形式化证明了并发理论的几个重要定理，其中包括我毕业导师 Davide Sangiorgi 两年前发表的最新成果。

本文简要介绍我自从2017年初以来新的变化和学业上的主要进展。

我目前属于博洛尼亚大学2014年入学，目前已在编外（Fuori corso / out of course）的学生。我的成绩单其实不算难看，很多课程都是满分30分，其中还有3门课是最高分（30L）可以体现出教授对我的充分肯定。其实我校计算机系的给分标准相对较高，学生通过数次考试以后最终拿到高分并不难，甚至某些选修课程只要完成了教授要求的全部工作即可轻松拿到满分，就好像只要肯选修就已经很值得表扬了似的。所以通过成绩单本身并不一定能看出学生的实际学习能力。但我眼下还真的是除了成绩单以外别的什么更像样的也没有了。