An engineered formal language to define and specify the meaning of programs

  • A set of strings conforming to a Formal Grammar
  • Specifies syntax and semantics
    • What seperation / level of abstraction between the semantics and syntax should exist?
    • Programs can “go wrong” (both erroneous or undefined) at either stage
    • Syntax and Semantics definitions correspond to their meaning in Linguistics
  • Specification should be unambigious!
    • i.e. semantics should be unambiguous, based on syntax
    • (Unambigious at Compiletime vs Runtime is part of the programming paradigm, e.g. FP is more compiletime unambigious oriented, whereas OOP is looser and you can only assume runtime unambiguity [alluding to Polymorphism / Dynamic Dispatch via vtable])

Programming Language Syntax

  • Syntax specifies allowed characters a program can contain
  • Syntax also specifies structure the allowed characters must obey
Link to original

Programming Language Semantics

  • For a “syntactically valid” program, what is the behavior?
  • How do we mathematically formalize the semantics of a program in an unambiguous way?
  • Formally precisely and unamiously specify what happens for a given program
  • Specification needs to be composition, defining what happens for a big program should be decomposed into what happens for the individual operations and subexpressions
  • Multiple strategies and formulation exists
  • Note Curry-Howard Correspondence / Curry-Howard-Lambek Correspondance
  • See also Formal Semantics

Semantics Example

This snippet is written in C

while (x < 7) ++x;

This program increments x until it is 7. However, we are making some assumptions. We assume that x is a variable that can be incremented. We assume that x is a variable that points to memory that is existent and valid and writeable. We assume that there is a notion of lines of code (locations in the “control flow graph”) in this program that we can loop through (as opposed to lambda calculus where there is no such notion, even though is still a valid program).

Link to original