Add lang.v, very rough verifier of tiny procedural language (not
completed, but enough for demonstration)