Archive

「我干了什么 究竟拿了时间换了什么」
2021

中国高等教育的系统性失败

The Systematic Failure of Higher Education in China


2020

Data Representation - Floating Point Numbers

「数据表示」浮点数


Data Representation - TODO

「数据表示」待写


Data Representation - Integer

「数据表示」整数


My Programming Languages Spectrum

我的编程语言光谱


2019

Peter John Landin

「计算机科学偶像」- 彼得·约翰·兰丁


My Spacemacs Workflow

From Vim to Spacemacs


把「终端下的 Vim」作为 macOS Finder 的打开方式

Open file with terminal Vim from the macOS Finder


「SF-QC」2 TypeClasses

Quickcheck - A Tutorial on Typeclasses in Coq


「SF-PLF」19 PE

Programming Language Foundations - Partial Evaluation


「SF-PLF」18 UseAuto

Programming Language Foundations - Theory And Practice Of Automation In Coq Proofs


「SF-PLF」17 UseTactics

Programming Language Foundations - Tactic Library For Coq


「SF-PLF」16 LibTactics

Programming Language Foundations - A Collection of Handy General-Purpose Tactics


「SF-PLF」15 Norm

Programming Language Foundations - Normalization of STLC


「SF-PLF」14 RecordSub

Programming Language Foundations - Subtyping with Records


「SF-PLF」13 References

Programming Language Foundations - Typing Mutable References


「SF-PLF」12 Records

Programming Language Foundations - Adding Records To STLC


「SF-PLF」11. TypeChecking

Programming Language Foundations - A Typechecker for STLC


「SF-PLF」10 Sub

Programming Language Foundations - Subtyping (子类型化)


「SF-PLF」9 MoreStlc

Programming Language Foundations - More on The Simply Typed Lambda-Calculus


「SF-PLF」8 StlcProp

Programming Language Foundations - Properties of STLC


「SF-PLF」7 Stlc

Programming Language Foundations - The Simply Typed Lambda-Calculus


「SF-PLF」6 Types

Programming Language Foundations - Type Systems


「SF-PLF」5 Smallstep

Programming Language Foundations - Small-Step Operational Semantics


「SF-PLF」4 HoareAsLogic

Programming Language Foundations - Hoare Logic as a Logic


「SF-PLF」3 Hoare2

Programming Language Foundations - Hoare Logic, Part II


「SF-PLF」2 Hoare

Programming Language Foundations - Hoare Logic, Part I


「SF-PLF」1 Equiv

Programming Language Foundations - Program Equivalence (程序的等价关系)


「SF-LC」16 Auto

Logical Foundations - More Automation


「SF-LC」15 Extraction

Logical Foundations - Extracting ML From Coq


「SF-LC」14 ImpCEvalFun

Logical Foundations - An Evaluation Function For Imp


「SF-LC」13 ImpParser

Logical Foundations - Lexing And Parsing In Coq


「SF-LC」12 Imp

Logical Foundations - Simple Imperative Programs


「SF-LC」11 Rel

Logical Foundations - Properties of Relations


「SF-LC」10 IndPrinciples

Logical Foundations - Induction Principles


「SF-LC」9 ProofObjects

Logical Foundations - The Curry-Howard Correspondence


「SF-LC」8 Maps

Logical Foundations - Total and Partial Maps


「SF-LC」7 Ind Prop

Logical Foundations - Inductively Defined Propositions (归纳定义命题)


「SF-LC」6 Logic

Logical Foundations - Logic in Coq


「SF-LC」5 Tactics

Logical Foundations - More Basic Tactics


「SF-LC」4 Poly

Logical Foundations - Polymorphism and Higher-Order Functions


「SF-LC」3 List

Logical Foundations - Working with Structured Data


「SF-LC」2 Induction

Logical Foundations - Proof by Induction


「SF-LC」1 Basics

Logical Foundations - Functional Programming in Coq


2018

Vim 与中文输入法

Using Vim with non-english input method


Avoiding success at all cost

Watching "Escape from the Ivory Tower: The Haskell Journey"


程序员中的梦想家

Dreamers among programmers


给《PWA 实战》一书写的推荐序


2017

「知乎」如何通俗地解释停机问题?

How to explain the Halting Problem?


「知乎」如何证明不可计算的函数比可计算的函数多?

Why is there more uncomputable functions?


「知乎」为什么 CSS 这么难学?

Why I dislike CSS as a programming language


Farewell, Flash. 感谢你,但这一次是真正的永别。

So long, and thanks for all the Flash


饿了么的 PWA 升级实践

Upgrading Ele.me to Progressive Web App


他是狗,你们便是苟奴隶


How does SW-Precache works?


「知乎」如何理解 document 对象是 HTMLDocument 的实例?

Why is document an instance of HTMLDocument?


下一代 Web 应用模型 —— Progressive Web App

The Next Generation Application Model For The Web - Progressive Web App


如何客观地评价「小程序」的体验?

Wechat Mini-Program vs. the Web, a UX comparison


2016

Service Worker 101「GDG DevFest 2016 北京」

🎞 Slides:Service Worker 101, Working Offline and Instant Loading (GDG DevFest 2016 Beijing)


Progressive Web Apps,复兴序章「QCon 上海 2016」

🎞 Slides:Progressive Web Apps, Make Web Great Again. (QCon Shanghai 2016)


Web 在继续离我们远去

After the release of Wechat Mini-Program


Progressive Web App 之我见

🎞 Slides:Progressive Web App, in my points of view


「译」React vs Angular 2:冰与火之歌

React versus Angular 2: There Will Be Blood


2015

都 2015 年了,CSS 怎么还是这么糟糕

🎞 Slides:CSS Still Sucks 2015


「译」iOS 9,为前端世界都带来了些什么?

iOS 9, Safari and the Web: 3D Touch, new Responsive Web Design, Native integration and HTML5 APIs


「知乎」设计师如何学习前端?

How designers learn front-end development?


「译」ES5, ES6, ES2016, ES.Next: JavaScript 的版本是怎么回事?

ES5, ES6, ES2016, ES.Next: What's going on with JavaScript versioning?


JavaScript 模块化七日谈

🎞 Slides:JavaScript Modularization Journey


聊聊「阿里旅行 · 去啊」—— 行业与战略

聊聊在线旅行行业与老东家的产品思路


JavaScript Module Loader

CommonJS,RequireJS,SeaJS 归纳笔记


See you, Alibaba

再见,阿里。


hUX 随想录(二):操作系统的浪漫主义 —— Metro 篇

信息、载体、抽象、UI 设计乱谈


Unix/Linux 扫盲笔记

不适合人类阅读,非常水的自我笔记


Definition of End to End User Scenarios


hUX 随想录(一):Digital native 数字原住民

两岁的侄女天天叫着手机手机


「知乎」如何评价 2015 年 3 月 9 日 Apple 春季发布会?

聊聊科技与新式奢侈品


Hello 2015

"Hello World, Hello Blog"


2014

「知乎」如何看待微信屏蔽快的打车事件?

恰有小感。


「知乎」你们觉得响应式好呢,还是手机和PC端分开来写?


「知乎」为什么阿里系软件体验都不好?

或许这就是所谓的企业 DNA


「知乎」对中国用户而言,Pure Android 是否比 MIUI 或 Flyme 体验更好?


「知乎」如何评价 MIUI 6?