Comment by Twey

3 months ago

In addition to the other comments here, note that in PL circles ‘syntax’ typically denotes _everything_ that happens before translation/execution, importantly including type checking. ‘Semantics’ is then about explaining what happens when the program is run, which can equivalently be described as deciding when two programs are equal, mapping programs to mathematical objects (whose ‘meaning’, or at least equality, is considered to be well understood), specifying a set of transformations the syntax goes through, et cetera.

In pure functional languages saying what value an expression will evaluate to (equivalently, explaining the program as a function of its inputs) is a sufficient explanation of the meaning of a program, and semantics for these languages is roughly considered to be ‘solved’. Open areas of study in semantics tend to be more about doing the same thing for languages that have more complicated effects when run, like imperative state update or non-local control (exceptions, async, concurrency).

There's some overlap in study: typically syntax is trying to reflect semantics in some way, by proving that programs accepted by the syntactic analysis will behave or not behave a certain way when run. E.G. Rust's borrow checker is a syntactic check that the program under scrutiny will not dereference an invalid pointer, even though that's a thing that is possible by Rust's runtime semantics. Compare to Java, which has no syntactic check for this because dereferencing invalid pointers is simply impossible according to the semantics of the JVM.