It is reasonable to hope that the relationship between computation and mathematical logic will be as fruitful in the next century as that between analysis and physics in the last. The development of this relationship demands a concern for both applications and mathematical elegance.
—— J. McCarthy
（希望下个世纪计算与数理逻辑的关系将会像上个世纪分析与物理的关系一样结出丰硕的果实是非常合理的。对这二者之间关系的研究成果即需要有各种应用也需要有数学的优雅。
"The theory of types brings in a new idea for the solution of paradoxes, especially suited to their intentional form. It consists in blaming the paradoxes not on the axioms that every propositional function defines a concept or class, but on the assumption that every concept gives a meaningful proposition, if asserted for any arbitrary object or objects as arguments"
—— K. Gödel
"In general the position as regards all such new calculi is this. – That one cannot accomplish by them anything that could not be accomplished without them. However, the advantage is, that, provided that such a calculus corresponds to the inmost nature of frequent needs, anyone who masters it thoroughly is able – without the unconscious inspiration which no one can command – to solve the associated problems, even to solve them mechanically in complicated cases in which, without such aid, even genius becomes powerless. . . . Such conceptions unite, as it were, into an organic whole, countless problems which otherwise would remain isolated and require for their separate solution more or less of inventive genius."
—— C. F. Gauss
We think we are creating the system for our own purposes. We believe we are making it in our own image... But the computer is not really like us. It is a projection of a very slim of ourselves: that portion devoted to logic, rule, and clarity.
—— Ellen Ullman
用一组基本的指令来编制一个计算机程序，非常类似于从一组公理来构造一个数学证明。
—— D.E.Knuth
【逻辑与计算】包括以下内容：
1. 数理逻辑中证明论和计算的关系，重点探讨集合论、类型论、范畴论和证明论之间的关系
2. 组合逻辑和λ-演算以及相关的函数式编程
3. 可计算函数问题，包括可计算性理论和计算复杂性理论
4. 和逻辑有关的程序设计语言的理论问题
本栏内容面向程序员等对逻辑和计算接口感兴趣的朋友，因此尽量避免涉及理论问题而以初级知识为主。对一些理论问题的探讨和论文的研究则放在姊妹小站【形式语法理论】的【计算基础】内。