程式理论的基本问题是如何建立一个相对完善的理论框架，为软体的设计和开发方法提供理论依据。这个框架应能提供有效地描述程式规约的语言；应能定义可操作的变换方法以便能规约构造可执行的程式；应能给出验证程式与其规约之间一致性的机制。

程式是用程式语言编写的，研究程式的规约、变换和验证，必须首先给出程式语言的语义。这种语义用数学方法刻画程式语句的加工过程，并将其执行结果形式化。所以，程式语义也叫形式语义。形式语义描述技术的本质是用严格的数学方法来研究程式。形式语义的研究始于20世纪60年代初期，ALGOL60 是第一个明确区分语法和语义的程式设计语言。J. McCarthyP. J.Landin，C.Strachy，D. ScottC. A. R. Hoare 和 E. W.Dijkstra 等学者，以及爱丁堡大学和维也纳 IBM 研究中心的计算机科学家们对程式语义的研究和发展都起过重要作用。程式语言的形式语义分为四类: 操作语义 ，模拟程式执行中计算系统的操作过程。指称语义，把程式作为论域间的泛函以便刻画程式的执行数学结果。公理语义，用公理化方法刻画程式与被加工数据的逻辑关係。代数语义，把程式执行的结果定义为满足某种公理体系的代数结构。程式理论对形式语义的需求，促进了论域、偏序以及範畴论等数学理论的发展;而形式语义理论的研究又促进了程式语言和程式设计方法的进步，例如: 在高级语言中广泛使用的过程说明和过程调用的精确概念和实现机制，就是在语义理论的研究中逐步明确的。

20世70年代初期，为了保证在作业系统中多个并行执行进程的正确性，导致了并发程式理论的产生。进入80年代以来，随着超大规模积体电路技术的日臻成熟，并行和分布计算机系统得到了迅速发展，特别是网际网路的出现和广泛使用，大大促进了并行程式理论的发展， 使之成为程式理论的一个重要分支。并发程式是包含多个没有因果关係的进程的程式。进程间的通信、同步和它们的并行执行是并发程式区别于顺序程式的基本操作。计算机科学中的并发概念是由Petri 在1962 年提出的。Hoare 和Milner在20世纪70年代后期，分别提出并发程式的CCS和CSP 模型，他们把输入输出以及并行执行作为基本语法成分引入程式设计语言，并使用结构操作语义方法定义模型中基本语法成分的操作语义，开创了用代数方法研究并发程式中通信和并行行为的领域。并发程式理论研究的内容包括: 如何刻画并行进程的行为，在什幺情况下它们可以互相模拟，研究各种通信及同步机制，以及死锁及活性，可观察性和发散性等并发现象。并发程式理论的研究加深了人们对并发系统的认识;其主要研究成果，例如， 关于通信和同步的概念，已作为基本语言成分在Ada，Occam和Java等程式语言中得到广泛套用。

进入20 世纪90年代，对控制系统的研究，例如对自动导航及核电站监测等控制系统的研究，引起了程式理论界的关注。这些系统的特点是: 它们都使用计算机进行实时控制; 对控制系统的安全性和可靠性要求高，控制系统的微小错误都将给经济和社会安全带来巨大的损失；系统中都存在两类不同对象：根据传统控制理论，使用微分方程刻画的连续现象和根据逻辑或代数方法， 使用电脑程式控制的离散型事件。这类系统又叫混合系统。混合系统的程式理论已成为研究热点。其基本目标是: 建立混合系统的计算模型，设计描述混合系统的高级语言，探索混合系统程式的设计和开发方法。在建立混合计算模型方面有三种不同的方法: 第一种称为逻辑型混合计算模型方法，其基本思想是在时态逻辑基础上引入时段和切变的概念。时段用于刻画系统在时间区间上的连续变化，切变则表示系统中离散事件间的时序关係。第二种是程式设计型混合模型方法，其目标是在CSP及ADA 等并发语言中引入连续变数及给定初值的微分方程 ，而语言中原有的通信、顺序及条件语句则用来表示系统中离散事件的关係。第三种方法是将自动机概念推广，把微分方程刻画的连续现象扩充为自动机的状态， 用自动机状态转移刻画离散事件间的关係。儘管混合系统理论发展的历史不长， 但它在一些重要的实时控制系统中已经得到了套用，显示出这些理论的生命力。

程式逻辑是描述和论证程式行为的逻辑，又称霍尔逻辑。程式和逻辑有着本质的联繫。如果把程式看成一个执行过程，程式逻辑的基本方法是先给出建立程式和逻辑间联繫的形式化方法，然后建立程式逻辑系统，并在此系统中研究程式的各种性质。用逻辑公式描述对输入和输出信息的要求，就可以建立逻辑公式和程式间的联繫，表示为

其中P和Q为有关程式变元的逻辑表达式；P称为S的前置条件；Q称为S的后置条件。此公式表示:如果程式S执行前程式变数的值满足前置条件P，且程式S终止，则程式S执行终止后，程式变数的值满足后置条件Q。如果进一步建立一套关于这类公式的推理规则，就能得到一个描述程式行为的逻辑系统，可以在此系统中研究程式的性质，这就是程式逻辑。　程式是在机器中执行的，程式中每个语句的执行导致机器状态的变化，因此程式的执行又可以由机器状态变化的序列表达。数理逻辑中的模态逻辑正是描述动态变元变化的一种逻辑，因此以模态逻辑为基础也可揭示逻辑与程式间的深刻联繫。

霍尔逻辑的缺点是其基本形式不能进行逻辑演算。为了克服这种缺点，人们20世纪80年代，提出了类型论方法以求为程式的设计和开发建立更完善的理论框架。比较典型的类型 理论是由P. Martin-L f 建立的，称为直觉主义类型论。它的基本思想是：精选一组类型(集合)作为程式规约，而它们的元素就是满足规约的程式；用一组规则定义类型与其元素间的隶属关係，这些规则即是从规约产生程式的变换规则，又是一阶(直觉主义) 逻辑的证明规则。因此，只要对给定的规约 (逻辑命题)进行证明，就可以构造出符合此规约的程式。这样，程式规约、变换、验证都寓于对规约的证明之中了。

计算理论（Theory of computation）是数学的一个领域，和计算机有密切关係。其中的理论是现代密码协定、计算机设计和许多套用领域的基础。该领域主要关心三个方面的问题：採用什幺计算模型（即形式语言、自动机）；解决哪些是能计算的、哪些是不能计算的（即可计算性理论及算法）；要用多少时间、要用多少存储（即计算複杂性理论）。这三方面的问题可以用一个问题来总括：“计算机的基础能力及限制到什幺程度？”

计算理论的“计算”并非指纯粹的算术运算（Calculation），而是指从已知的输入通过算法来获取一个问题的答案（Computation），因此，计算理论属于计算机科学和数学。为了对计算进行严谨的研究，计算机科学家会将计算以数学的方式抽象化，称为计算模型。有几种在使用的计算模型，其中最出名的是图灵机。计算机科学家研究图灵机的原因是它很容易叙述，可以分析，用来证明结果，而且用此模式呈现了许多强而有力的计算模型（引用邱奇－图灵论题）。图灵机有潜在的，数量无限的记忆能力，这似乎是不可能达到的，不过所有图灵机解决的可判定性问题都只需要有限量的记忆能力。因此理论上，任何可以用图灵机解决的（可判定性）问题都只需要有限量的记忆能力。