欢迎大家赞助一杯啤酒🍺 我们准备了下酒菜：Formal mathematics/Isabelle/ML, Formal verification/Coq/ACL2, C++/F#/Lisp
在政企项目的煎熬中享受过，在互联网的鸡血中沉醉过，如今是移动互联网一迷途小coder。
AtlasLee，黎展波，夏日的猫。
Atlas不是地图，是希腊神话里背负苍天的泰坦。
黎展波不是泰坦，是一只猫。
夏日是找不到猫的。嘘，它们都在树荫底下睡觉呢。
<discussion>characters_max=300</discussion>
