一些胡思乱想
码农一年

我参加的第一次workshop

nonoob posted @ Sat, 25 Aug 2012 00:54:44 +0800 in Nonsense , 1313 readers

Verified Software Workshop原本昨天就有了,但是昨天因为学校对硕士有歧视所以没赶上校车最终没去(不过今天才听说假期就没有接送学生的校车,而校车只为接送老师;我们能上车是老师给我们的福利);今天才去,多少有些后悔。

是MSRA主办的,四年一届,今年找了华师当搭档了。不过这个workshop没有任何门槛,报个名都可以进;所以我这种沽名钓誉的人就屁颠屁颠的跑去了。

请到了1980年图灵奖得主Tony Hoare来,微软真有心!总是在书中看到霍尔逻辑,在网页上看到霍尔的头像,今天终于见到本尊了;这种欣喜之情就和一个虔诚的佛教徒看到观音显圣一样!CS真是门年轻的学科,用到的理论都还这么新,大神一般的人物竟然还有这么多,而且层出不穷。不过听学长说Hoare讲课经常跑题,动不动就说“Let‘s go back to the point”;唉,毕竟人老了嘛。我错过了昨天的演讲,今天只听到他的几句总结。不过在panel discussion蔡老师问如何做research时,他说“Do something different”;我倒觉得似曾相识(我是不是又yy了?);只是目前还做得太少,没有多少心得。不过有一种传言这些德高望重的人多半是被逼着参加某某活动来撑场面的,谁又能指望他们在这种workshop上有新的idea呢?Hoare现在是微软剑桥研究院的,难道说……?看来我想多了。不过话说回来,即使没有什么实质的帮助,但鉴于这只是一个workshop,并且在场人当中不乏我这种业外人士;有一个重量级的人物在,并且还说了些,对我们总是有鼓舞的作用的。华师出力也不少,软件学院院长何积丰教授是中科院院士;后来才知道他和Hoare有过不少合作成果——这大概才是这次workshop在华师的最重要原因吧。

听讲座时我想起巴别塔这个词;尽管演讲者用的都是英语,但是还是可以凭各个人的口音(包括英国、美国的差异)大体推断出其国籍。而在用到各种术语时,经常存在两种概念几乎表达同种意思的时候,可双方都坚持用自己的说法;也有不少两种概念都用同一个说法表达的情况,谁都以为对方说的是自己的意思。这或许是上帝为了误导我们故意混乱我们的,可谁又能保证如果不存在这么多混乱这个领域可以取得现有的发展呢?语言或表述的不同的确给人与人之间带来了隔阂,那workshop大家都聚在一起是不是正是为了弥补交流的不便导致的误解呢?再想想,各种编程语言的存在是不是也给coder之间的交流带来了麻烦呢?如果没有这些语言的分歧,咱码农的世界又会怎样?估计早就没落了吧!!!flexible、efficient往往不可兼得啊。

另外我现在觉得Verified Software并不是最接近程序本质的东西,至少说从目前的研究结果来看是这样的;尽管检测程序的正确性是软件非常重要的部分,但现实的软件如此复杂以致我们根本没有办法有一套全面的验证方法来解决问题,大部分结果还都只是停留在toy一样的层次上。反之,这样一个原本应当非常形式化的内容,到头来却用到了非常多的工程上的方法。另一个让我稍有不可思议的是,这个领域的researcher们都尽可能回避函数式编程;程序验证这块在最符合图灵模型的命令式语言上还没有搞定,在函数式上的确更大打折扣了。可是,函数式语言是搞程序语言理论不可绕过的啊。

另一个感触,学术界的研讨果然太空洞了!看不见,摸不着;花非花,雾非雾,夜半来,天明去;总有种“幽暗昏惑而无物以相之”之感。这个感觉是否正确目前我还没法断言,但我感觉至少和老秦描述的他参加的几次开发者大会很不同。提问时有人指出在现实公司中没听说过真正使用到程序验证方法的(尽管事实上可以在小范围内有),这种类似砸场子的干活倒也引起了演讲者们的窘迫!到底有没有用,只能留给后人说去了;不过我有种不祥的预感(但由于我现在的立身出世,我希望我的感觉大错特错)。

在这个workshop能坚持一天的最猥琐的一个理由是这里有免费餐券,尤其是晚上的自助餐。貌似我现在已经有些习惯了这种蹭饭蹭住的生活了,终于可以揣度到贪官污吏们的心理了,hooray!不过还是感觉有些对不起微软,给我们提供了这样的优待,我却从来没说过她什么好话过,吃人家嘴软了?不过我承认绝不是IT评论中的那样吃干饭的,微软的研究院的确很牛逼,微软对软件工程功不可没(按道理我没资格评论这些>_<)。

感觉workshop上演讲者主要还是将自己的团队近期的成果(说白一点就是conference上已中的或待中的paper);如果本人不做演讲,参加workshop之前最好把感兴趣的文章多看几遍然后不懂的地方问演讲者。如果可以预测workshop中自己发言的机会很少,那还是离它远点好;把这当科普讲堂可走错地方了。

Avatar_small
Garfileo said:
Sat, 25 Aug 2012 08:39:24 +0800

我是外行,所以不是很清楚程序验证搞的是什么。

不过,就 FP 编程来说,我觉得这种编程方式中引入了许多可以提高程序正确性的明确的法则,这是 FP 非常好的一面。用那套法则来写程序,可以抛弃一些很含糊的设计模式之类的东西。

极端一些来说,如果大家都像玩数学的那样玩编程,那么验证程序的正确性不就如同验证一个数学定理那样的有章可循了么。

Avatar_small
nonoob said:
Sat, 25 Aug 2012 11:53:26 +0800

@Garfileo: 说实在的我也没搞清楚程序验证究竟是什么。fp我接触不多,且只写过一点lisp和scala的玩具代码,所以我没什么深入的感悟。


Login *


loading captcha image...
(type the code from the image)
or Ctrl+Enter