On checked exceptions and proof obligations
Checked exceptions are a much vilified feature of Java, despite theoretical reasons why it should be a really good idea. The tension is between these two lines of reasoning: Well-written programs handle all possible edge-cases, working around them when possible and gracefully dying if not. It's hard to keep track of all possible exceptions, so […]