Proving Programs: Why, When, How?