Text this: An elementary and unified approach to program correctness