Comment by scns

Lazyness as the motivation for creating machines/typecheckers to do the boring work.