LOCATINO'S NOTE

I. 基准代码

一份基准代码（Codebase），多份部署（deploy）

12-Factor应用通常会使用版本控制系统加以管理，如Git, Mercurial, Subversion。一份用来跟踪代码所有修订版本的数据库被称作代码库（code repository, code repo, repo）。

在类似SVN这样的集中式版本控制系统中，基准代码就是指控制系统中的这一份代码库；而在Git那样的分布式版本控制系统中，基准代码则是指最上游的那份代码库。

基准代码和应用之间总是保持一一对应的关系：

• 一旦有多个基准代码，就不能称为一个应用，而是一个分布式系统。分布式系统中的每一个组件都是一个应用，每一个应用可以分别使用 12-Factor 进行开发。
  多个应用共享一份基准代码是有悖于12-Factor原则的。解决方案是将共享的代码拆分为独立的类库，然后使用依赖管理策略去加载它们。
• 尽管每个应用只对应一份基准代码，但可以同时存在多份部署。每份 部署 相当于运行了一个应用的实例。通常会有一个生产环境，一个或多个预发布环境。此外，每个开发人员都会在自己本地环境运行一个应用实例，这些都相当于一份部署。

所有部署的基准代码相同，但每份部署可以使用其不同的版本。比如，开发人员可能有一些提交还没有同步至预发布环境；预发布环境也有一些提交没有同步至生产环境。但它们都共享一份基准代码，我们就认为它们只是相同应用的不同部署而已。

II. 依赖

显式声明依赖关系（ dependency ）

大多数编程语言都会提供一个打包系统，用来为各个类库提供打包服务，就像 Perl 的 CPAN 或是 Ruby 的 Rubygems 。通过打包系统安装的类库可以是系统级的（称之为 “site packages”），或仅供某个应用程序使用，部署在相应的目录中（称之为 “vendoring” 或 “bunding”）。

12-Factor规则下的应用程序不会隐式依赖系统级的类库。 它一定通过 依赖清单 ，确切地声明所有依赖项。此外，在运行过程中通过 依赖隔离 工具来确保程序不会调用系统中存在但清单中未声明的依赖项。这一做法会统一应用到生产和开发环境。

例如， Ruby 的 Bundler 使用 Gemfile 作为依赖项声明清单，使用 bundle exec 来进行依赖隔离。Python 中则可分别使用两种工具 – Pip 用作依赖声明， Virtualenv 用作依赖隔离。甚至 C 语言也有类似工具， Autoconf 用作依赖声明，静态链接库用作依赖隔离。无论用什么工具，依赖声明和依赖隔离必须一起使用，否则无法满足 12-Factor 规范。

显式声明依赖的优点之一是为新进开发者简化了环境配置流程。新进开发者可以检出应用程序的基准代码，安装编程语言环境和它对应的依赖管理工具，只需通过一个 构建命令 来安装所有的依赖项，即可开始工作。例如，Ruby/Bundler 下使用 bundle install，而 Clojure/Leiningen 则是 lein deps。

12-Factor 应用同样不会隐式依赖某些系统工具，如 ImageMagick 或是curl。即使这些工具存在于几乎所有系统，但终究无法保证所有未来的系统都能支持应用顺利运行，或是能够和应用兼容。如果应用必须使用到某些系统工具，那么这些工具应该被包含在应用之中。

III. 配置

在环境中存储配置

通常，应用的 配置 在不同 部署 (预发布、生产环境、开发环境等等)间会有很大差异。这其中包括：

• 数据库，Memcached，以及其他 后端服务 的配置
• 第三方服务的证书，如 Amazon S3、Twitter 等
• 每份部署特有的配置，如域名等

有些应用在代码中使用常量保存配置，这与 12-Factor 所要求的代码和配置严格分离显然大相径庭。配置文件在各部署间存在大幅差异，代码却完全一致。

判断一个应用是否正确地将配置排除在代码之外，一个简单的方法是看该应用的基准代码是否可以立刻开源，而不用担心会暴露任何敏感的信息。

需要指出的是，这里定义的“配置”并不包括应用的内部配置，比如 Rails 的 config/routes.rb，或是使用 Spring 时 代码模块间的依赖注入关系 。这类配置在不同部署间不存在差异，所以应该写入代码。

另外一个解决方法是使用配置文件，但不把它们纳入版本控制系统，就像 Rails 的 config/database.yml 。这相对于在代码中使用常量已经是长足进步，但仍然有缺点：总是会不小心将配置文件签入了代码库；配置文件的可能会分散在不同的目录，并有着不同的格式，这让找出一个地方来统一管理所有配置变的不太现实。更糟的是，这些格式通常是语言或框架特定的。

12-Factor推荐将应用的配置存储于 环境变量 中（ env vars, env ）。环境变量可以非常方便地在不同的部署间做修改，却不动一行代码；与配置文件不同，不小心把它们签入代码库的概率微乎其微；与一些传统的解决配置问题的机制（比如 Java 的属性配置文件）相比，环境变量与语言和系统无关。

配置管理的另一个方面是分组。有时应用会将配置按照特定部署进行分组（或叫做“环境”），例如Rails中的 development,test, 和 production 环境。这种方法无法轻易扩展：更多部署意味着更多新的环境，例如 staging 或 qa 。 随着项目的不断深入，开发人员可能还会添加他们自己的环境，比如 joes-staging ，这将导致各种配置组合的激增，从而给管理部署增加了很多不确定因素。

12-Factor 应用中，环境变量的粒度要足够小，且相对独立。它们永远也不会组合成一个所谓的“环境”，而是独立存在于每个部署之中。当应用程序不断扩展，需要更多种类的部署时，这种配置管理方式能够做到平滑过渡。

IV. 后端服务

把后端服务(backing services)当作附加资源

后端服务是指程序运行所需要的通过网络调用的各种服务，如数据库（MySQL，CouchDB），消息/队列系统（RabbitMQ，Beanstalkd），SMTP 邮件发送服务（Postfix），以及缓存系统（Memcached）。

类似数据库的后端服务，通常由部署应用程序的系统管理员一起管理。除了本地服务之外，应用程序有可能使用了第三方发布和管理的服务。示例包括 SMTP（例如 Postmark），数据收集服务（例如 New Relic 或 Loggly），数据存储服务（如 Amazon S3），以及使用 API 访问的服务（例如 Twitter, Google Maps, Last.fm）。

12-Factor 应用不会区别对待本地或第三方服务。 对应用程序而言，两种都是附加资源，通过一个 url 或是其他存储在 配置 中的服务定位/服务证书来获取数据。12-Factor 应用的任意 部署 ，都应该可以在不进行任何代码改动的情况下，将本地 MySQL 数据库换成第三方服务（例如 Amazon RDS）。类似的，本地 SMTP 服务应该也可以和第三方 SMTP 服务（例如 Postmark ）互换。上述 2 个例子中，仅需修改配置中的资源地址。

每个不同的后端服务是一份 资源 。例如，一个 MySQL 数据库是一个资源，两个 MySQL 数据库（用来数据分区）就被当作是 2 个不同的资源。12-Factor 应用将这些数据库都视作 附加资源 ，这些资源和它们附属的部署保持松耦合。

部署可以按需加载或卸载资源。例如，如果应用的数据库服务由于硬件问题出现异常，管理员可以从最近的备份中恢复一个数据库，卸载当前的数据库，然后加载新的数据库 – 整个过程都不需要修改代码。

V. 构建，发布，运行

严格分离构建和运行

基准代码 转化为一份部署(非开发环境)需要以下三个阶段：

• 构建阶段 是指将代码仓库转化为可执行包的过程。构建时会使用指定版本的代码，获取和打包 依赖项，编译成二进制文件和资源文件。
• 发布阶段 会将构建的结果和当前部署所需 配置 相结合，并能够立刻在运行环境中投入使用。
• 运行阶段 （或者说“运行时”）是指针对选定的发布版本，在执行环境中启动一系列应用程序 进程。
  代码被构建，然后和配置结合成为发布版本

12-factor 应用严格区分构建，发布，运行这三个步骤。 举例来说，直接修改处于运行状态的代码是非常不可取的做法，因为这些修改很难再同步回构建步骤。

部署工具通常都提供了发布管理工具，最引人注目的功能是退回至较旧的发布版本。比如， Capistrano 将所有发布版本都存储在一个叫 releases 的子目录中，当前的在线版本只需映射至对应的目录即可。该工具的 rollback 命令可以很容易地实现回退版本的功能。

每一个发布版本必须对应一个唯一的发布 ID，例如可以使用发布时的时间戳（2011-04-06-20:32:17），亦或是一个增长的数字（v100）。发布的版本就像一本只能追加的账本，一旦发布就不可修改，任何的变动都应该产生一个新的发布版本。

新的代码在部署之前，需要开发人员触发构建操作。但是，运行阶段不一定需要人为触发，而是可以自动进行。如服务器重启，或是进程管理器重启了一个崩溃的进程。因此，运行阶段应该保持尽可能少的模块，这样假设半夜发生系统故障而开发人员又捉襟见肘也不会引起太大问题。构建阶段是可以相对复杂一些的，因为错误信息能够立刻展示在开发人员面前，从而得到妥善处理。

VI. 进程

以一个或多个无状态进程运行应用

运行环境中，应用程序通常是以一个和多个 进程 运行的。

最简单的场景中，代码是一个独立的脚本，运行环境是开发人员自己的笔记本电脑，进程由一条命令行（例如python my_script.py）。另外一个极端情况是，复杂的应用可能会使用很多 进程类型 ，也就是零个或多个进程实例。

12-Factor 应用的进程必须无状态且 无共享。 任何需要持久化的数据都要存储在 后端服务 内，比如数据库。

内存区域或磁盘空间可以作为进程在做某种事务型操作时的缓存，例如下载一个很大的文件，对其操作并将结果写入数据库的过程。12-Factor应用根本不用考虑这些缓存的内容是不是可以保留给之后的请求来使用，这是因为应用启动了多种类型的进程，将来的请求多半会由其他进程来服务。即使在只有一个进程的情形下，先前保存的数据（内存或文件系统中）也会因为重启（如代码部署、配置更改、或运行环境将进程调度至另一个物理区域执行）而丢失。

源文件打包工具（Jammit, django-compressor） 使用文件系统来缓存编译过的源文件。12-Factor 应用更倾向于在 构建步骤 做此动作——正如 Rails资源管道 ，而不是在运行阶段。

一些互联网系统依赖于 “粘性 session”， 这是指将用户 session 中的数据缓存至某进程的内存中，并将同一用户的后续请求路由到同一个进程。粘性 session 是 12-Factor 极力反对的。Session 中的数据应该保存在诸如 Memcached 或 Redis 这样的带有过期时间的缓存中。

VII. 端口绑定

通过端口绑定(Port binding)来提供服务

互联网应用有时会运行于服务器的容器之中。例如 PHP 经常作为 Apache HTTPD 的一个模块来运行，正如 Java 运行于 Tomcat 。

12-Factor 应用完全自我加载 而不依赖于任何网络服务器就可以创建一个面向网络的服务。互联网应用 通过端口绑定来提供服务 ，并监听发送至该端口的请求。

本地环境中，开发人员通过类似http://localhost:5000/的地址来访问服务。在线上环境中，请求统一发送至公共域名而后路由至绑定了端口的网络进程。

通常的实现思路是，将网络服务器类库通过 依赖声明 载入应用。例如，Python 的 Tornado, Ruby 的Thin , Java 以及其他基于 JVM 语言的 Jetty。完全由 用户端 ，确切的说应该是应用的代码，发起请求。和运行环境约定好绑定的端口即可处理这些请求。

HTTP 并不是唯一一个可以由端口绑定提供的服务。其实几乎所有服务器软件都可以通过进程绑定端口来等待请求。例如，使用 XMPP 的 ejabberd ， 以及使用 Redis 协议 的 Redis 。

还要指出的是，端口绑定这种方式也意味着一个应用可以成为另外一个应用的 后端服务 ，调用方将服务方提供的相应 URL 当作资源存入 配置 以备将来调用。

VIII. 并发

通过进程模型进行扩展

任何计算机程序，一旦启动，就会生成一个或多个进程。互联网应用采用多种进程运行方式。例如，PHP 进程作为 Apache 的子进程存在，随请求按需启动。Java 进程则采取了相反的方式，在程序启动之初 JVM 就提供了一个超级进程储备了大量的系统资源(CPU 和内存)，并通过多线程实现内部的并发管理。上述 2 个例子中，进程是开发人员可以操作的最小单位。

扩展表现为运行中的进程，工作多样性表现为进程类型。

在 12-factor 应用中，进程是一等公民。12-Factor 应用的进程主要借鉴于 unix 守护进程模型 。开发人员可以运用这个模型去设计应用架构，将不同的工作分配给不同的 进程类型 。例如，HTTP 请求可以交给 web 进程来处理，而常驻的后台工作则交由 worker 进程负责。

这并不包括个别较为特殊的进程，例如通过虚拟机的线程处理并发的内部运算，或是使用诸如 EventMachine, Twisted, Node.js 的异步/事件触发模型。但一台独立的虚拟机的扩展有瓶颈（垂直扩展），所以应用程序必须可以在多台物理机器间跨进程工作。

上述进程模型会在系统急需扩展时大放异彩。 12-Factor 应用的进程所具备的无共享，水平分区的特性 意味着添加并发会变得简单而稳妥。这些进程的类型以及每个类型中进程的数量就被称作 进程构成 。

12-Factor 应用的进程 不需要守护进程 或是写入 PID 文件。相反的，应该借助操作系统的进程管理器(例如 systemd ，分布式的进程管理云平台，或是类似 Foreman 的工具)，来管理 输出流 ，响应崩溃的进程，以及处理用户触发的重启和关闭超级进程的请求。

IX. 易处理

快速启动和优雅终止可最大化健壮性

12-Factor 应用的 进程 是 易处理（disposable）的，意思是说它们可以瞬间开启或停止。 这有利于快速、弹性的伸缩应用，迅速部署变化的 代码 或 配置 ，稳健的部署应用。

进程应当追求 最小启动时间 。 理想状态下，进程从敲下命令到真正启动并等待请求的时间应该只需很短的时间。更少的启动时间提供了更敏捷的 发布 以及扩展过程，此外还增加了健壮性，因为进程管理器可以在授权情形下容易的将进程搬到新的物理机器上。

进程 一旦接收 终止信号（SIGTERM） 就会优雅的终止 。就网络进程而言，优雅终止是指停止监听服务的端口，即拒绝所有新的请求，并继续执行当前已接收的请求，然后退出。此类型的进程所隐含的要求是HTTP请求大多都很短(不会超过几秒钟)，而在长时间轮询中，客户端在丢失连接后应该马上尝试重连。

对于 worker 进程来说，优雅终止是指将当前任务退回队列。例如，RabbitMQ 中，worker 可以发送一个NACK信号。 Beanstalkd 中，任务终止并退回队列会在worker断开时自动触发。有锁机制的系统诸如 Delayed Job 则需要确定释放了系统资源。此类型的进程所隐含的要求是，任务都应该 可重复执行 ， 这主要由将结果包装进事务或是使重复操作 幂等 来实现。

进程还应当在面对突然死亡时保持健壮，例如底层硬件故障。虽然这种情况比起优雅终止来说少之又少，但终究有可能发生。一种推荐的方式是使用一个健壮的后端队列，例如 Beanstalkd ，它可以在客户端断开或超时后自动退回任务。无论如何，12-Factor 应用都应该可以设计能够应对意外的、不优雅的终结。Crash-only design 将这种概念转化为 合乎逻辑的理论。

X. 开发环境与线上环境等价

尽可能的保持开发，预发布，线上环境相同

从以往经验来看，开发环境（即开发人员的本地 部署）和线上环境（外部用户访问的真实部署）之间存在着很多差异。这些差异表现在以下三个方面：

时间差异： 开发人员正在编写的代码可能需要几天，几周，甚至几个月才会上线。
人员差异： 开发人员编写代码，运维人员部署代码。
工具差异： 开发人员或许使用 Nginx，SQLite，OS X，而线上环境使用 Apache，MySQL 以及 Linux。
12-Factor 应用想要做到 持续部署 就必须缩小本地与线上差异。 再回头看上面所描述的三个差异:

缩小时间差异：开发人员可以几小时，甚至几分钟就部署代码。
缩小人员差异：开发人员不只要编写代码，更应该密切参与部署过程以及代码在线上的表现。
缩小工具差异：尽量保证开发环境以及线上环境的一致性。
将上述总结变为一个表格如下：

12-Factor 应用的开发人员应该反对在不同环境间使用不同的后端服务 ，即使适配器已经可以几乎消除使用上的差异。这是因为，不同的后端服务意味着会突然出现的不兼容，从而导致测试、预发布都正常的代码在线上出现问题。这些错误会给持续部署带来阻力。从应用程序的生命周期来看，消除这种阻力需要花费很大的代价。

与此同时，轻量的本地服务也不像以前那样引人注目。借助于Homebrew，apt-get等现代的打包系统，诸如Memcached、PostgreSQL、RabbitMQ 等后端服务的安装与运行也并不复杂。此外，使用类似 Chef 和 Puppet 的声明式配置工具，结合像 Vagrant 这样轻量的虚拟环境就可以使得开发人员的本地环境与线上环境无限接近。与同步环境和持续部署所带来的益处相比，安装这些系统显然是值得的。

不同后端服务的适配器仍然是有用的，因为它们可以使移植后端服务变得简单。但应用的所有部署，这其中包括开发、预发布以及线上环境，都应该使用同一个后端服务的相同版本。

XI. 日志

把日志当作事件流

日志 使得应用程序运行的动作变得透明。在基于服务器的环境中，日志通常被写在硬盘的一个文件里，但这只是一种输出格式。

日志应该是 事件流 的汇总，将所有运行中进程和后端服务的输出流按照时间顺序收集起来。尽管在回溯问题时可能需要看很多行，日志最原始的格式确实是一个事件一行。日志没有确定开始和结束，但随着应用在运行会持续的增加。

12-factor应用本身从不考虑存储自己的输出流。 不应该试图去写或者管理日志文件。相反，每一个运行的进程都会直接的标准输出（stdout）事件流。开发环境中，开发人员可以通过这些数据流，实时在终端看到应用的活动。

在预发布或线上部署中，每个进程的输出流由运行环境截获，并将其他输出流整理在一起，然后一并发送给一个或多个最终的处理程序，用于查看或是长期存档。这些存档路径对于应用来说不可见也不可配置，而是完全交给程序的运行环境管理。类似 Logplex 和 Fluentd 的开源工具可以达到这个目的。

这些事件流可以输出至文件，或者在终端实时观察。最重要的，输出流可以发送到 Splunk 这样的日志索引及分析系统，或 Hadoop/Hive 这样的通用数据存储系统。这些系统为查看应用的历史活动提供了强大而灵活的功能，包括：

• 找出过去一段时间特殊的事件。
• 图形化一个大规模的趋势，比如每分钟的请求量。
• 根据用户定义的条件实时触发警报，比如每分钟的报错超过某个警戒线。

XII. 管理进程

后台管理任务当作一次性进程运行

进程构成（process formation）是指用来处理应用的常规业务（比如处理 web 请求）的一组进程。与此不同，开发人员经常希望执行一些管理或维护应用的一次性任务，例如：

运行数据移植（Django 中的 manage.py migrate, Rails 中的 rake db:migrate）。
运行一个控制台（也被称为 REPL shell），来执行一些代码或是针对线上数据库做一些检查。大多数语言都通过解释器提供了一个 REPL 工具（python 或 perl） ，或是其他命令（Ruby 使用 irb, Rails 使用 rails console）。
运行一些提交到代码仓库的一次性脚本。
一次性管理进程应该和正常的 常驻进程 使用同样的环境。这些管理进程和任何其他的进程一样使用相同的 代码 和 配置 ，基于某个 发布版本 运行。后台管理代码应该随其他应用程序代码一起发布，从而避免同步问题。

所有进程类型应该使用同样的 依赖隔离 技术。例如，如果Ruby的web进程使用了命令 bundle exec thin start ，那么数据库移植应使用 bundle exec rake db:migrate 。同样的，如果一个 Python 程序使用了 Virtualenv，则需要在运行 Tornado Web 服务器和任何 manage.py 管理进程时引入 bin/python 。

12-factor 尤其青睐那些提供了 REPL shell 的语言，因为那会让运行一次性脚本变得简单。在本地部署中，开发人员直接在命令行使用 shell 命令调用一次性管理进程。在线上部署中，开发人员依旧可以使用ssh或是运行环境提供的其他机制来运行这样的进程。

不知道从什么时候开始，你开始兢兢业业地工作，你开始对每一件遗憾的事物释怀，你开始觉得现在的生活也还不错。
但是你就是不能满血，始终笼罩着一层无法驱散的惶惶不安，始终肩负着某些摆脱不了的沉重，好像总有一些不可知的事情会发生，没人给你兜底，也没有能够应对的踏实。虽然每天都能正常入眠，却不能真正休息，总有一些疲惫常驻后台。
不知道是从哪里开始出了问题，但你就是累了。
你开始想象平行世界的另一个你过着怎样的生活。

What is LIFE ?

影片中有一处男主在格陵兰岛租车时面临的选择：红色或者蓝色，明显是致敬《黑客帝国》中救世主尼奥对于红蓝药丸的选择。

当感觉生活甚至世界有些不对的时候，你面前有两个药丸，也就是两种选择，

红色告诉你所想要的真相但真相或许是你难以接受的，蓝色药丸吃下便忘记这一切第二天像往常一样起床但将永远不会接触到真相。

正如日常生活就像一个牢笼，困在里面也不自知，当然也不会想逃出来。

男主选择租下了红色的汽车，踏上旅程，告别了幻想，补完了自己的的灵魂。

我们每天重复着昨天的生活，随着惯性推进每一步，几乎丧失思考的空间和时间，人生匆匆忙忙，可是又毫无意义。

好像想要寻找什么打破这种真实到不真实的生活，急需一个突破口让某种能量冲出体内。

男主义无反顾地跳上了直升机，见过了格陵兰的鲨鱼、冰岛的火山、喜马拉雅的雪豹，

人生即是带着自己不甘堕落的心，去绽放不一样的生命之花。

大多数人按照我们所安排的路线生活，害怕探索其它路线，但也会有一些人，他们并不满足于被设定的生活轨迹，冲破我们设置的重重阻碍，意识到自由意志是天赐之物的人，才明白只有在奋力抗争后才知道如何善用之。

To see the world, things dangerous to come to.
To see behind walls.
To draw closer.
To find each other and to feel.
That's the purpose of LIFE.

你是否也曾有那么恍惚一刻做着虚幻的白日梦想？

Long long the stream that runs to sea Listen to my plea Listen willow and weep for me
Wisper to the wind and say that love has sinned Left my heart a-breaking

计算模型大致可以分为两类，λ演算和其他…好吧，也许Post的产生式系统和Herbrand-Goedel等式属于前者，但是毋庸置疑所有总所周知并且被广泛接受的模型比如图灵机，RAM和λ演算可不是一类的。Guy Blelloch将这类差异划分为语言和机器。基于机器的模型全部是在无界内存下的有限控制理论基础上讨论的。它依靠程序员去管理内存，实现一切结构，并且没有记号，没有解释器这样的机制在运行时改变程序；机器模型全部是非冯诺依曼机，因为它们没有存储程序的思想。基于语言的模型，相较之下，没有把程序和数据分开，并提供建立真实语言的基础，直接且没有编码。这似乎是一个λ演算的决定性优势：尽管机器模型出现在我们教材的前几章，但是他们本质上没有实际重要性，而λ演算对编程和逻辑系统的机械化来说是直接有用的。但现在机器模型仍然处于主宰地位，特别是算法和复杂度的领域，λ演算却作为冷门怪异的知识仅仅被计算机科学家的一小部分人研究。这是怎么回事？

遇到这个问题时，我的同事（至少在理论这边）认为这个问题一点意思都没有，回避了这个问题，因为“所有计算模型都需要多项式时间”，so who care? 好吧，如果你的工作在多项式因子的复杂度完成，并且你只关心对自然数（或者其他有限对象）的计算，那我猜这问题确实无所谓。你把某个问题算了一遍，对于那些利益相关的对象是如何在某个模型上表现的毫不关心，那细节的确无所谓。
但是明显地这些模型有所谓，事实上，说这话的同事在任何情况下都不会考虑经典的机器模型作为他工作的基础！毫无疑问，如果这些模型都是等价的话，选什么没关系，所以我们都可以选择λ演算，对吧？好吧，确实是这样。显而易见，有些模型是比其他模型更合适的！怎么会这样？

一个原因是许多工作并不是取决于多项式因子的（有人可能更认为，大部分都不是的）。所以对于这些目的，模型是有所谓的。另一方面，没有人在实际工作中用“正式的”模型。没人用图灵机码去描述算法，甚至RAM代码也没有用（Knuth是个例外）。反而，他们用的是类Algol语言，或者类C语言，或者类似的命令式编程符号。也就是说，他们用的是编程语言，而不是机器！他们当然这么做。但那又为什么强调机器模型呢？他们写的那些语言意味着什么？

答案是这些语言是由描述这样那样的类Algol语言如何对应于这样那样的RAM代码或者图灵机码的解释器定义的。这种表述虽不正式，但已足够准确使人明白。关键是，你推理的不是你写的代码，而是编译器写的代码，因为正式来讲目标代码才是“真正的”代码，伪代码只是提供一个方便。所以在工作中，你脑子里必须有一个编译器：它对一切你写的代码都清楚明白，知道如何翻译成，比如RAM代码。这并不是太难，因为伪代码简单，简单到你可以直接在脑子里编译它。这种方式不错，但是会逐渐出现问题，因为它约束了我们表达算法的语言从而限制了我们能够方便表达和分析的算法的范围。

那为什么坚持使用这样麻烦的方式呢？一个原因是，传统。我的导师用它，所以我也用它。或者，如果你想要发论文，你最好用一种评审熟悉的风格写。
一个更实际的原因是，机器模型是描述计算开销的基础。计算的一“步”就是机器的一步，我们通过估算解决同一问题算法的步数来比较算法（取决于乘法因子，大部分情况下）。只要我们能够“手工编译”类Algol语言到机器码，我们就可以给一个比汇编语言高级的语言赋一个开销，还可以对各类算法做合理的比较。这种方法良好的满足了我们的需求，但是现在它开始没那么管用了（并行是一个原因，但还有许多其他理由）。

有一个替代选项，为我们书写的语言提供了开销语义，并且直接地在这个基础上开展我们的分析，不用迎合编译器或者依赖机器。简而言之我们采用了计算的语言模型，而非机器模型，生活更美好！表达算法有更多的方式，还简化了分析算法的方法。

要用这种方式我们需要我们使用的语言一个开销语义。这也就是λ演算的优势，因为它是描述计算的语言模型的典型例子。简单来说，λ演算的右箭头标记表示一步推导，写作M→M’，表示M程序经过一步计算之后的结果为M’程序。执行过程直接由我们写出，并且模型还为计算步骤提供了良定义的标记，我们可以数出来获取程序的时间复杂度。数十年的经验表明这种方法扩展到了真实语言。

有什么缺点呢？我个人找不出什么缺点。我一直很困惑，觉得λ演算应该在算法圈子里被接受。正如任何机器模型都被当做完美的计算基础，而业界的行为都显明机器模型对实际完成的工作有很大的限制！
唯一的原因我觉得，除去强大的社会影响，就是停滞不前，还未发现λ演算里关于开销的概念对算法分析的适合。（一个研究员最近告诉我“你可以塞一头大象在β推导里！”，然而他还是没法解释我哪错了。）一种验证这个观点的方法就是，定义出一个λ演算到RAM代码的编译器，确保λ演算里的抽象步骤能被RAM在常量时间里实现（不考虑输入大小，只考虑静态程序的大小）。Blelloch和Greiner在90年代初已经精确的完成了这项分析。详见Guy’s web page。

之后的博文里我会深入的考察这些思想，并且表明（通过检查Blelloch的工作）λ演算不仅可以作为一个串行算法的良好模型，对并行算法也是一样！而且我们可以轻松地把模型扩展为具有重要抽象能力的语言比如高阶函数或者不用优化就能表达和分析算法。

翻译 by locatino
原文

##Question##
下面是一段非常神奇的**C++**代码。因为一些莫名其妙的原因，处理排序后的数据比没有排序的数据奇迹般的快了许多倍。

1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35

#include <algorithm>
#include <ctime>
#include <iostream>

int main()
{
// Generate data
const unsigned arraySize = 32768;
int data[arraySize];

for (unsigned c = 0; c < arraySize; ++c)
data[c] = std::rand() % 256;

// !!! With this, the next loop runs faster
std::sort(data, data + arraySize);

// Test
clock_t start = clock();
long long sum = 0;

for (unsigned i = 0; i < 100000; ++i)
{
// Primary loop
for (unsigned c = 0; c < arraySize; ++c)
{
if (data[c] >= 128)
sum += data[c];
}
}

double elapsedTime = static_cast<double>(clock() - start) / CLOCKS_PER_SEC;

std::cout << elapsedTime << std::endl;
std::cout << "sum = " << sum << std::endl;
}

• 没有std::sort(data, data + arraySize);这句代码，程序运行了11.54秒。
• 有上述那句代码，程序运行了1.93秒。

最开始，我以为这只是特定语言或者编译器的反常现象。所以我在Java里也试了。

1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36

import java.util.Arrays;
import java.util.Random;

public class Main
{
public static void main(String[] args)
{
// Generate data
int arraySize = 32768;
int data[] = new int[arraySize];

Random rnd = new Random(0);
for (int c = 0; c < arraySize; ++c)
data[c] = rnd.nextInt() % 256;

// !!! With this, the next loop runs faster
Arrays.sort(data);

// Test
long start = System.nanoTime();
long sum = 0;

for (int i = 0; i < 100000; ++i)
{
// Primary loop
for (int c = 0; c < arraySize; ++c)
{
if (data[c] >= 128)
sum += data[c];
}
}

System.out.println((System.nanoTime() - start) / 1000000000.0);
System.out.println("sum = " + sum);
}
}

结果也类似，只不过速度差异没有那么夸张。
我最初以为是因为排序把数据带入了高速缓存里，但马上就发现这个想法多么愚蠢，因为数组是运行时生成的。

• 发生了什么事？
• 为什么排序后的数组比没有排序的数组处理起来快？
• 代码仅仅把数据元素单独的相加，数据元的顺序应该没有影响才对。

##什么是分支预测？##
请参考下图铁轨分岔路：

为了方便说明这个程序问题，假设我们回到了1800年代——在无线电或者其他长距离通信方式发明之前。
你是一名操作员，你听到了一辆火车正在驶来。你不知道它要走哪个方向。你停下了火车去问列车长他要走哪个方向。然后你正确地设置了分岔口的开关。


火车重，并且惯性大。所以它们启动和停下需要花费大量的时间。


那有没有更好的方式？你来猜火车会走哪条路！

• 如果你猜对了，火车就继续走。
• 如果你猜错了，那列车长会停车，退回，训斥你重新操作分岔开关。然后火车重新驶向另一条路。

如果你每次都猜对，火车将永远不用停下来。

如果你老是猜错，火车将会花费大量的时间停下来，退回，重启。

观察下列if语句：在处理器层面上，它是一条分支指令：

假设你是一个处理器并且你发现了一个分支指令。你不知道接下来会执行哪条指令。你怎么办？你挂起了程序，等待之前的指令执行完毕。然后你顺着正确的分支继续执行。


现代处理器结构复杂并且拥有长流水线。所以它们启动和停止需要花费大量的时间。


那有没有更好的方式？你来猜接下来会执行哪条分支！

• 如果你猜对了，你就继续执行。
• 如果你猜错了，你需要刷新指令流水线并回退到分支语句。然后你重新执行正确地分支。

如果你每次都猜对，执行将永远不用停止。
如果你老是猜错，你将花费大量的时间停止，回退，重启。

这就是分支预测。我承认上面的比喻不是最合适的，因为火车只需要打一面标识行进方向的旗子就可以了。但是计算机里，处理器不到最后一刻是不会知道该进入哪条分支的。
所以你该如何选择猜测方案来最小化火车回退重启的次数呢？你观察之前的历史！如果火车99%的情况下走左边，那么你就猜左。反之，你就猜右。如果它每三次就走其中某个特定的方向，你就猜它接下来也是这样……
换句话说，你试图找出一个模式并遵循它。这差不多就是分支预测器的工作方式。
大部分应用都有可良好预测的分支。所以现代分支预测器差不多可以达到>90%的命中率。但是当面临无可预测的分支并且毫无规律可循的情况下，分支预测器基本上形同虚设。

深入阅读：“Branch predictor” article on Wikipedia。

##根据以上所说，罪魁祸首就是这条if语句##

1
2

if (data[c] >= 128)
sum += data[c];

注意到数据是均匀的分布在0到255之间。所以当数据从小到大排序之后，差不多前部分有一半的数据没有进入if语句的分支里。之后，剩下的数据全部进入if语句的分支里。
这对分支预测器是十分友好的，因为程序会连续的进入同一分支多次。一个简单的饱和计数器都可以正确的预测分支，除了刚好程序转向时的那几次失败。
###简单视图化###

1
2
3
4
5
6
7

T = branch taken
N = branch not taken

data[] = 0, 1, 2, 3, 4, ... 126, 127, 128, 129, 130, ... 250, 251, 252, ...
branch = N N N N N ... N N T T T ... T T T ...

= NNNNNNNNNNNN ... NNNNNNNTTTTTTTTT ... TTTTTTTTTT (easy to predict)

然而，当数据完全随机，分支预测器毫无用处因为它无法预测随机数据。因此，大概有50%的错误预测。

1
2
3
4

data[] = 226, 185, 125, 158, 198, 144, 217, 79, 202, 118, 14, 150, 177, 182, 133, ...
branch = T, T, N, T, T, T, T, N, T, N, N, T, T, T, N ...

= TTNTTTTNTNNTTTN ... (completely random - hard to predict)

###所以应该如何是好？###
如果编译器没法把分支优化成可良好预测，你可以用一些技巧优化，如果你愿意为性能牺牲可读性的话。
将：

1
2

if (data[c] >= 128)
sum += data[c];

替换为：

1
2

int t = (data[c] - 128) >> 31;
sum += ~t & data[c];

这样就用一些位操作消除了分支。（上述方法并不等价于原来的if语句。仅仅是在这个例子中跟原来的if语句效果一样。）

###测试环境：Core i7 920 @ 3.5 GHz###
C++ - Visual Studio 2010 - x64 Release

1
2
3
4
5
6
7
8
9
10
11

// Branch - Random
seconds = 11.777

// Branch - Sorted
seconds = 2.352

// Branchless - Random
seconds = 2.564

// Branchless - Sorted
seconds = 2.587

Java - Netbeans 7.1.1 JDK 7 - x64

1
2
3
4
5
6
7
8
9
10
11

// Branch - Random
seconds = 10.93293813

// Branch - Sorted
seconds = 5.643797077

// Branchless - Random
seconds = 3.113581453

// Branchless - Sorted
seconds = 3.186068823

观测结果：

• 使用分支语句：排序和未排序的数据处理效率差异巨大。
• 消除分支语句：排序和未排序的数据没有区别。
• 使用C++时，消除分支语句的执行速度是比使用分支处理排序后的数据的速度慢一点的。

所以一般的最佳做法是避免在重要的循环中使用依赖数据特性的分支。

整个西方哲学只不过是一连串柏拉图的注脚而已。


人的认知状态分成不同等级：从最低级的想像，到信念，再到思想，最高的认知是理解。


洞穴假说：每一次上升，每一次转向光，他都会眼睛痛，恨不得返回从前的状态。但一旦他习惯于新的明亮世界，他会为自己脱离以前的黑暗愚昧状态而庆幸，并可怜仍然生活在那里的同伴。


有多少人反思过自己的伦理道德标准的有效性和有限性。


所谓“解救”，是让人把头转过去，将灵魂进行转向。转了向，就看到了火。而这其实就是使灵魂得到了光明。我们经常讲的“启蒙”一次就是enlightment，字面意义是“在灵魂中(en)有了光(light)”。


把哲学分门别类是柏拉图的学生亚里士多德的事。


四大主德：正义，勇敢，节制，智慧。


一种观点可能被驳倒，但这不等于说这种观点一定是错的。


按照苏格拉底的观点，任何惩罚，应当是教育性的。唯有当某种惩罚是为了改进某个人的灵魂，才有正当性。


人们称颂正义，并不是因为他们认为正义好于不正义，而是因为他们乐于别人对他们正义。


正确的理解是，正义或道德自身就是幸福的内在构成部分，幸福不是正义的处在目的，而是依附于正义的。


苏格拉底，柏拉图，亚里士多德都是反民主的。在某种程度上是现代民主制的敌人。


有些人在理想城邦中的地位较低，由此会心生不满。但这只是因为他们不明白，他们的地位其实是他们自然地应当占有的位置。真理只能为社会中的一小部分人发现并掌握。社会中的大部分人都生活在洞穴之中，没有办法自己发现真理。


在柏拉图看来，底阶层受到一点欺骗却可以按自然而生活，这应是值得的。


凡是人类拥有的恶，奥林匹斯山上的诸神无不具有。


人类有一种惰性，即灵魂很容易被同化为我们所看到，所听到的东西。


悲剧是危险的，它破坏了对有关道德问题寻求单一理性答案的努力。


专制主义也有比较温和的形式。那就是，个人是整体的成员，但国家的功能与目的只是要促进公民的福祉，国家并无除此而外的独立利益。这种温和的形式也可叫做权威主义或家长制。


柏拉图确定了灵魂的三个部分：欲望，理性和激情。


所谓的意志薄弱现象的出现并不是因为人们对快乐的欲求战胜了人们对好或善的欲求，而是因为人类根本不知道什么是好，没有关于好的真正的知识。


所以，当人们以为出现意志薄弱的情况时，其实所犯的真正错误是无知。


对“什么是x”这类问题的回答应当找到一个形式(eidos)F。它呈现在一切被称为F的事物中，是所有F事物都共有的F这一属性。因为它，F的事物才成为F。一个适当的定义必须找到这样的形式。这一定义不是说明该术语的日常用法，而是要揭示该术语所代表的客观的共同本质。


总之，知道某个事物是否具有某种属性并不是古代哲人所关心的事情。他们所关注的是不希望看到人们处于混乱，困惑的状态，而要让人们能够去除无知，并且自我意识到自己处于明白的状态。


历史上的苏格拉底亦有名言曰，光喝水不喝酒是产生不了智慧的。


真正的哲学家是没有统治欲望的。


“善自身在理智领域中与理智和可知事物的关系，就如同太阳在可见世界中视力和可见事物的关系一样”。理智把握可知事物即形式，得到知识，就正如视力在可见世界中观看可感事物而得到感觉一样。


形式是用来说明具体事物的“是”或存在(being)的；而善的形式则是用来说明形式的“是”或存在。


在柏拉图看来不懂数学是无法超越可感世界而进入可知世界的。


如果说一个人能够思想了，或开始思想了，那就是说他或她能够解脱习俗樊篱的束缚，破除对日常经验的顺随，而开始对其自身所处的世界进行批判性的思考。


教育在柏拉图那里不是对知识和信息的获得，不是把知识放进灵魂。教育是让灵魂转向其应该关注的对象和方向上去，让它能使用自身的能力去看。


数与计算是为一切思想，一切技艺所共同使用的东西。


数学自然能够将人从可感事物上升到形式。

Quaint child, old-fashioned Alice, lend your dream: I would be done with modern story-spinners, Follow with you the laughter and the gleam: Weary I am, this night, of saints and sinners. We have been friends since Lewis and old Tenniel Housed you immortally in red and gold. Come! Your naivete is a spring perennial: Let me be young again before I am old.
You are a glass of youth: this night I choose Deep in your magic labyrinths to stray, Where rants the Red Queen in her splendid hues And the Write Rabbit hurries on his way. Let us once more adventure, hand in hand: Give me belief again—— in Wonderland!

——Vincent Starret, in Brillig

最近在学习函数式编程，又想顺便学下大名鼎鼎的Python ，遂把The little schemer里的scheme代码全部用Python实现了一遍。
函数式编程的精髓当然是传说中的lambda表达式，本来打算用Python lambda实现scheme代码，没想到网上一查API，却发现Python lambda实在是做的弱到不行……不能缩进（一个lambda函数只能写在一行），只能用if…else…，只能写一条语句等等。

“Why can’t lambda expressions contain statements?

Python lambda expressions cannot contain statements because Python’s syntactic framework can’t handle statements nested inside expressions. However, in Python, this is not a serious problem. Unlike lambda forms in other languages, where they add functionality, Python lambdas are only a shorthand notation if you’re too lazy to define a function.

Functions are already first class objects in Python, and can be declared in a local scope. Therefore the only advantage of using a lambda instead of a locally-defined function is that you don’t need to invent a name for the function – but that’s just a local variable to which the function object (which is exactly the same type of object that a lambda expression yields) is assigned!”

为啥lambda表达式不能包含语句？

以上是Python官方FAQ给出的答复：lambda表达式就是给你偷懒少打几个字用的，不支持在语句中嵌套表达式。

基本上Python Lambda就应用在以下场景：

1
2
3
4
5

f = lambda x, y: x + y
g = lambda x: x + 1

print(f(1, 2))
print(g(1))

这匿名函数还tm有个名字。
或者你可以节约名字:

1
2

print((lambda x, y: x + y)(1, 2))
print((lambda x: x + 1)(1))

是不是觉得还不如这样：

1
2

print(1 + 2)
print(1 + 1)

不得不说Python lambda简直是鸡肋。

但是，你注意到Python lambda支持if…else…语句了吗，scheme也只有cond…else这一种控制语句，却是非常优美的函数式PL。
所以我试着用if…else…来搞点名堂。

1

lambda x: True if x % 2 == 0 else False

上面的函数判断一个数是不是偶数，其中if…else…是Python lambda的标准用法。
冒号后面接返回值return-expression，接着是该返回值的条件cond-expression，接着else，然后是else的返回值。
Python lambda总共以下2种写法，一种是不含if…else…的，一种是包含if…else…的：

1
2

lambda <args>: <return-expression>
lambda <args>: <return-expression> if <cond-expression> else <return-expression>

第二条语句的**”< return-expression > if < cond-expression > else < return-expression >”** 整体也是一个return-expression。
所以我们可以在else后的return-expression中嵌套return-expression来完成复杂的条件判断语句：

1

lambda <args>: <return-expression> if <cond-expression> else (<return-expression> if <cond-expression> else <return-expression>)

如果想要在匿名函数中做一些除了return-expression，其他事情（比如说print()）,应该怎么写？
确实不太好写，不过我还是想出了一个非常投机取巧的办法：

1

lambda x: True if x % 2 == 0 and print(x) == None else x")

上面这个函数不仅返回了x的值，并且还打印了x，这里我把需要执行的语句(print())转换成了逻辑表达式，而且是一个永远为真的表达式，它一定会执行，并且对业务的逻辑判断没有影响。
前提是你必须准确的知道需要执行的语句的返回值，才能写出永远为真的表达式。再写一个例子：

1

lambda x, l: l if l.insert(0,x) == None else l

上面这个函数把元素x插入到l的头部，并返回l。
通过这种投机取巧的办法我们可以大大扩充Python lambda的功能。

Python lambda还可以返回异常：

1

lambda x: TypeError("x is zero.") if x == 0 else 5/x

那么迭代（循环）怎么写？
迭代确实是一个难题，scheme这样没有迭代的语句是怎么实现迭代的？递归。
首先我们先用常规函数的递归实现迭代：

1
2
3
4
5
6
7
8
9
10
11
12
13

#求和递归版本
def sum_recur(l):
if len(l) == 0:
return 0
else:
return l[0] + sum_recur(l[1:])

#求和迭代版本
def sum_iter(l):
sum = 0
for i in l:
sum += i
return sum

以上2个函数均实现了list l中元素求和，功能上是等价的。

但是匿名函数要递归调用自身难度很高。
以下可能有点高能，初学者慎入。
首先要知道，lambda表达式也是一个return-expression。所以我们还可以在lambda中返回lambda：

1

lambda <args>: lambda <args>: <return-expression>

先看看下面这个函数

1
2
3
4

def sum(f):
return lambda l:0 if len(l) == 0 else l[0] + f(f)(l[1:])

print(sum(sum)([1,2]))

这个函数接受一个自身作为参数，返回值是一个求和函数，也就是实际的递归本体，即sum(sum) = lambda l:0 if len(l) == 0 else l[0] + sum(sum)(l[1:]),如此实现递归调用自身。
我们先把sum(f)转换成lambda函数：

1
2
3
4

def sum(f):
return lambda l:0 if len(l) == 0 else l[0] + f(f)(l[1:])

lambda f: lambda l:0 if len(l) == 0 else l[0] + f(f)(l[1:])

上述2个函数式功能是等价的,返回值都相同，只是一个有名字而已，匿名函数没有名字如何调用自身？也是通过函数的参数，并且直接使用自身的定义，所以我们可以令**sum(sum)**为：

1
2
3
4

sum(lambda f: lambda l:0 if len(l) == 0 else l[0] + f(f)(l[1:]))
#第二个sum，也就是作为参数的sum已被等价的lambda替换，
#现在我们再来替换第一个sum
(lambda f: lambda l:0 if len(l) == 0 else l[0] + f(f)(l[1:])) (lambda f: lambda l:0 if len(l) == 0 else l[0] + f(f)(l[1:]))

这就完成了匿名函数递归调用自身。测试：

1
2
3

g = (lambda f: lambda l: 0 if len(l) == 0 else l[0] + f(f)(l[1:])) (lambda f: lambda l: 0 if len(l) == 0 else l[0] + f(f)(l[1:]))

print(g([1,2,3]))

接下来优化一下~

注意到

1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17

#f(f)(x)
#等价于
#lambda x: f(f)(x)

#那么我们可以把上面出现的f(f)都用参数替换，然后传一个lambda x: f(f)(x)作为参数即可
g = (lambda f: lambda l: 0 if len(l) == 0 else l[0] + (lambda x: f(f)(x))(l[1:])) (lambda f: lambda l: 0 if len(l) == 0 else l[0] + (lambda x: f(f)(x))(l[1:]))


g = (lambda y: (lambda f:lambda l: 0 if len(l) == 0 else l[0] + f(l[1:]))(lambda x: y(y)(x)))(lambda y: (lambda f:lambda l: 0 if len(l) == 0 else l[0] + f(l[1:]))(lambda x: y(y)(x)))
#注意：
lambda f:lambda l: 0 if len(l) == 0 else l[0] + f(l[1:])
#此函数就是真正的业务递归过程，其他结构均是辅助，我们可以提取出来
job = lambda f:lambda l: 0 if len(l) == 0 else l[0] + f(l[1:])

g = (lambda y: job(lambda x: y(y)(x)))(lambda y: job(lambda x: y(y)(x)))

print(g([1,2,3]))

这个g就是传说中的上古神器Y-Combinator！它就是一个通用的匿名函数递归公式。

至此，我们已经把Python lambda的功能扩充的基本和普通函数差不多了（额，可能还差一点）。
而且所有函数全部一行完成，然而并没有什么卵用。

本书教授了如何理解多线程执行和如何解决同步问题。尤其推荐给自学和初学者。
里面一步步教导读者解决一系列的经典和不那么经典的同步问题。内容非常有趣。
下载链接：http://www.greenteapress.com/semaphores/downey08semaphores.pdf

函数（Function）太棒了。如果我们创造一门只有函数的语言会如何？
对象（Object）太棒了。如果我们创造一门一切都是对象的语言会如何？
惰性求值（Lazy evaluation）太棒了。如果我们创造一门所有类型都是惰性的语言会如何？

极端主义编程（Extremist Programming, 与极限编程无关）是一种奉行某种思想（Principle），用它来衡量其他一切事物并将它应用在任何地方的行为。等到尘埃落定之后，人们通常会对着这种极端主义方式思考，“额，这确实很有趣，但是把X用在Y里明显不恰当。你需要换一种正确的方式来达到目的！”

上面这段话的意思是：有时候你需要使用错误的工具工作，因为你并不知道用这工具是不是正确的。如果你不到处使用函数，你也许就不明白将一个函数作为另一个函数的参数有怎样的功效，也许就不明白Cheap Lambda表达式的意义。如果你不到处使用对象，你也许就不理解其实整型和类的实例其实都是对象。如果你不到处使用惰性求值，你也许就没意识到其实函数的纯粹性（Purity）其实是一种更加重要的语言特征。

这就引出了两个建议：

1. 当学习一种新的思想时，尝试将它到处运用一番。这样你就可以很快的知道它什么时候适用什么时候不适用，即使你对它的第一印象全是错的。（另一方面，如果你没有进行这样错误的尝试的话，你将失去对它适用范围理解的机会。）

2. 当试图理解某种思想的本质时，一个极端的例子是最清晰明了的。如果你想知道使用惰性求值编程是怎么样的，你会使用Haskell，而不是其他的非强制惰性求值的语言。即使这样极端的系统并不实用，但它确实能够更好的体现本质。

极端主义在很多场合并不恰当，但是对于那些有趣的，小巧的项目或者研究，它真的能够教会你许多。给我印象最深的一件事情就是我去年和Adam Chlipala的合作。当时我们用Coq进行一些证明，我用的是中规中矩的方式，先一步一步推导要证的雏形，然后使用Ltac自动证明。Adam告诉我：“你应该一开始就自动证明的，不用麻烦的做手工推导”。真是醍醐灌顶：我就是不够极端！

文件（File）太棒了。如果我们创造一种一切都是文件的操作系统会如何？
Cons结构（Cons cell）太棒了。如果我们创造一种一切都由Cons组成的编程语言会如何？
数学（Mathematics）太棒了。如果我们创造一种一切都是数学说了算的编程语言会如何？
数组（Array）太棒了。如果我们创造一种一切都是数组的语言会如何？

翻译 by locatino
原文链接http://blog.ezyang.com/2012/11/extremist-programming/