一个朋友海归了 (转载)# Returnee - 海归
h*i
1 楼
【 以下文字转载自 SanFrancisco 讨论区 】
发信人: soldiercrab (老军医专治装B文学小青年), 信区: SanFrancisco
标 题: 一个朋友海归了
发信站: BBS 未名空间站 (Wed Dec 23 17:10:53 2009, 美东)
当年我们一起学习形式化方法。我的数学基础巨差（当年犯傻选了Software
Engineering方向，修了一堆嘛用没有的课。早知道就该选CS+Math方向了），读
Nielson et al的Principles of Program Analysis时极其郁闷，觉得欧洲淫都是大尾
巴狼，不说人话。一点不明白为啥人要把看似简单直观的程序分析转化为公式成堆的格
点方程。我朋友非常耐心地给我讲解背后的关窍，直到我理解了作者的思路。当初如何
利用群对称化简状态空间的复杂度也是他手把手教我的。十足的好银呐。他的理想是把
形式方法带入中国的航空航天工业（NASA是形式化方法的大用户之一），所以今年拿了
PhD后就立马和他老婆回国，进了一家跟航空有关的的学校。一个人一辈子心无旁骛地
做一件心自己喜欢的事情不容易。但愿他做出
发信人: soldiercrab (老军医专治装B文学小青年), 信区: SanFrancisco
标 题: 一个朋友海归了
发信站: BBS 未名空间站 (Wed Dec 23 17:10:53 2009, 美东)
当年我们一起学习形式化方法。我的数学基础巨差（当年犯傻选了Software
Engineering方向，修了一堆嘛用没有的课。早知道就该选CS+Math方向了），读
Nielson et al的Principles of Program Analysis时极其郁闷，觉得欧洲淫都是大尾
巴狼，不说人话。一点不明白为啥人要把看似简单直观的程序分析转化为公式成堆的格
点方程。我朋友非常耐心地给我讲解背后的关窍，直到我理解了作者的思路。当初如何
利用群对称化简状态空间的复杂度也是他手把手教我的。十足的好银呐。他的理想是把
形式方法带入中国的航空航天工业（NASA是形式化方法的大用户之一），所以今年拿了
PhD后就立马和他老婆回国，进了一家跟航空有关的的学校。一个人一辈子心无旁骛地
做一件心自己喜欢的事情不容易。但愿他做出