What is this fraction-like "discrete mathematics"–style notation used for formal rules?
This is a standard notation for an inference rule.  The premises are put above a horizontal line, and the conclusion is put below the line.  Thus, it ends up looking like a "fraction", but with one or more logical propositions above the line and a single proposition below the line.  If you see a label (e.g., "LET" or "VAR" in your example) next to it, that's just a human-readable name to identify the particular rule.

You might also see this referred to as natural deduction or Gentzen-style natural deduction.

This is a common notation in the programming languages literature.  You'll see it all over the place.  It's very convenient for the kinds of conclusions and recursive-structured proofs that arise in that field.

You'll see this notation used to express axioms/rules. You can think of each axiom as a template with "meta-variables" (e.g., expr); you can replace each meta-variable with some syntax from the programming language (e.g., any expression that is valid in the programming language), and you'll get an instance of the rule.  The inference rule promises that if all of the propositions are above the line are true (for some instance of the template, where you consistently replace each metavariable with the same value throughout the rule), then the proposition below the line will be true, too.