Reasoning about sequential programs: Ancient and modern