把思想写成精确符号、使推理能够逐步核对的愿望很老。17 世纪末，莱布尼茨（Leibniz）设想过一种“普遍文字”（characteristica universalis），以及配套的推理演算（calculus ratiocinator）：思想写成符号，推理变成计算，争论的双方只需说一句“我们来算一算”（Calculemus）。

两百年后，弗雷格（Frege）在 1879 年的《概念文字》（Begriffsschrift）里真的造出了这样一门语言，它是现代逻辑的起点之一。他在序言里说，日常语言的推理里，常有没被察觉的前提悄悄混进来；他想要的是一条没有缝隙的推理链，每一步都看得见用了什么。 [约定] 阅读约定 也采用了这种证明写法：每个隐含的前提都要摆到台面上。

莱布尼茨的梦想没有完全实现。20 世纪的哥德尔（Gödel）和图灵（Turing）证明了，有些问题原则上就不能靠“算一算”来裁决。在程序语言理论中， [定义] 一步归约 与 [定义] 类型与类型判断 用规则精确定义运行和类型， [推论] 类型安全 则从这些规则证明良类型程序不受阻，是这种可核对推理的一个小例子。