To talk a little about Michael Madsen, an example is the behavior of the ++ operator. Informally, we describe a statement using plain English. For example:
If x is an int variable, ++x causes x to increment by one.
(I do not accept any integer overflows and ++x returns nothing)
In formal semantics (and I will use operational semantics), we would work a little. First, we need to define the concept of types. In this case, I will assume that all variables are of type int . In this simple language, the current state of a program can be described by a repository, which is a mapping of variables into values. For example, at some point in the program, x might be 42, and y be -5351. The storage can be used as a function - for example, if the storage s has a variable x with a value of 42, then s(x) = 42 .
Also, the current state of the program includes the rest of the program instructions that we must execute. We can relate this as <C, s> , where C is the remaining program and s is the repository.
So, if we have the state <++x, {x -> 42, y -> -5351}> , this is unofficially the state where the only remaining command to execute is ++x , the variable x has the value 42, and the variable y has a value of -5351 .
Then we can determine the transitions from one state of the program to another - we describe what happens when we take the next step in the program. So, for ++ we could define the following semantics:
<++x, s> --> <skip, s{x -> (s(x) + 1)>
To some extent, unofficially, by running ++x , the next skip command, which has no effect, and the variables in the store remain unchanged, except for x , which now has a value that originally had a value plus one. Some work remains to be done, for example, to determine the notation that I used to update the repository (which I did not do so that this answer does not increase!). Thus, a specific instance of a general rule can be:
<++x, {x -> 42, y -> -5351}> --> <skip, {x -> 43, y -> -5351}>
Hope this gives you this idea. Note that this is just one example of formal semantics — along with operational semantics — axiomatic semantics (which often uses Hoar’s logic) and denotational semantics, and probably a lot more than I am not familiar with.
As I mentioned in a comment on another answer, the advantage of formal semantics is that you can use them to prove certain properties of your program, for example, that it ends. Besides the fact that your program does not exhibit bad behavior (for example, without interruption), you can also prove that your program behaves as needed, proving that your program meets the specified specification. Having said that, I never thought about pointing and checking the program for anything that is convincing, since I found a specification, usually just rewritten in logic by the program, so the specification is also wrong.