形式语义（formal semantics），理学-计算机科学技术-计算机软件-软件基础理论-程序理论-形式语义，人们希望编程语言和程序所具有的，严格的、形式化（数学）的语义定义。在计算领域，人们最早关注的是编程语言和程序的语义。程序的意义就是它在计算机上运行时的行为和表现。由于程序是用编程语言描述的，如果把编程语言的语义定义好，也就定义了所有程序的语义。在传统上，编程语言的语法早已有严格的定义技术，但其语义通常只有自然语言的解释，有时附上一些代码实例说明。程序语言和程序牵涉多个相关方，包括语言设计者、编译器（或解释器）开发者、程序开发工作者（语言的使用者）和最终用户。如果不同相关方对编程语言语义的理解出现偏差，就可能造成语言的定义、实现、编程和实际应用之间脱节，并可能造成严重后果，带来无法估量的损失。程序之所以很难理解，根源在于程序代码的静态形式与执行时的动态行为之间的关系并不显见。故人们希望形式语义定义比较清晰简单，容易理解和使用，这样才能避免误解。