6.2. Catch or declare🔗

Laurel enforces catch-or-declare, the discipline Java applies to its checked exceptions. A procedure that declares no throws may not let an exception escape, whether thrown directly or propagated from a callee, and a procedure declaring throws T may only let exceptions escape whose type is a subtype of T.

composite ArithError {}
composite ParseError {}

procedure wrongThrows()
  throws (e: ArithError)
  opaque
{
  var e: ParseError := new ParseError;
  throw e
  // error: procedure 'wrongThrows' may throw 'ParseError', which is not a
  // subtype of its declared `throws` type 'ArithError'
};

The check is about the program as you wrote it rather than about how it lowers, so it runs during resolution and reports at the offending throw or call. Whether the source language requires catch-or-declare is a separate question: procedures coming from Python or JavaScript carry a throws clause too, even though neither language has that surface construct.