The author criticizes some design choices made by the paper's authors as not being simple enough. However, in fairness to that paper, it's aiming for dependentl

The author criticizes some design choices made by the paper's authors as not being simple enough. However, in fairness to that paper, it's aiming for dependently typed lambda calculus and, for reasons of continuity of exposition, is probably making sub-optimal choices up front that pay off later. The distinction between inferable and checkable types, for example, doesn't really pay off until you need to do beta-reduction in the type checker. The author of the present article has the luxury of stopping early, with just an STLC implementation.