我理解，理论计算机科学主要从以下两个方面探索计算的数学本质：

第一、研究如何表达计算的过程，即计算的模型。比如已知的三个等价模型，图灵机模型、函数模型和演算模型。

第二、研究各种计算问题在计算模型上的可计算性（能否计算）和计算的复杂性（资源消耗）。

而为了达到上述目的，必须充分调动各种必要的数学工具，构建必要的数学理论，这个活动中最为核心的方法是形式化。

此外，我认为必须注意物理学、生命科学等研究对象本身就包含着计算能力和计算形式的学科的发展。在它们的基础上可能获得新的理论突破。

比如大家熟知的丘齐－图灵论题。丘齐论题认为，凡可计算函数与Lamda演算等价，而图灵论题认为，可计算函数与图灵机可计算等价。所以丘齐－图灵论题认为，可计算性和图灵可计算性是等价的，并断言若一个计算问题不存在能行的图灵机算法解，则不可能在任何计算模型中找到这样的解。

1994年，Shor提出了一个在量子计算的模型下的能在多项式时间内完成的大数分解算法，而大数分解一般被认为没有多项式时间的图灵机算法解。这表明，量子计算可能会颠覆丘奇－图灵论题。

PS：倒数第二段“并断言若一个计算问题能行的图灵机算法解，则不可能在任何计算模型中找到这样的解。”是不是少了几个字？

还有，欧洲和北美的理论计算机研究，方向有很大的不同，现在美国的理论计算机偏重于算法的研究，所以近些年来，各种算法的提出都源于美国；而欧洲的理论计算机，更偏重于形式化的研究，VDM，Z Notation，B－Method，CPS，CCS，Process Algeba，Pi Calculus这些形式化模型，全部出于欧洲。