serpent_skis

> This is not true if a, b and c are unsigned

True, but this is not valid if they are signed, either. Take

  a = INT_MIN
  b = 1
  c = 2

Then

  a < b + c

is true. But

  a - b < c

invokes undefined behavior.

Edit: missed

> Say that a, b and c are small integers (we don't worry about addition overflow)

Ah, well that makes this example vacuously true, however I'm not sure what the utility in that restriction is. We've only moved the goalposts from "bend[ing] the rules of arithmetic around zero" to bending the rules of arithmetic outside of "small integers".

The reason for using a match statement, even though there is only “one” case, is because it’s matching against a complex and (as you mentioned) deeply nested pattern. Lines 43-56 match the current AST node against the pattern (shown here as pseudo-python):

  with open(_) as f:
    _ = f.read()

(Where _ can be anything, and f can be any name). The traditional alternative to lines 43-56 would be dozens of lines that check the top level of the AST, and if that matches against what the top level of the pattern is expecting, diving one layer deeper and checking that level against the next level of the pattern, etc, until you reach the leaves of your pattern. Once your familiar with pattern matching syntax, this is much easier to quickly read/grok/audit.

What a coincidence, I just started watching his Programming Languages Theory lectures. Seems like a wonderful professor.