The use of revert(), assert(), and require() in Solidity, and the new REVERT opcode in the EVM

Thanks for this detailed writeup! The distinction between require and assert should also get clearer with the introduction of the SMT checker for assert (currently experimental with pragma experimental SMTChecker;). Note that you should not use assert blindly for overflow checking but only if you think that previous checks (either using ifor require) would make an overflow impossible.