New example: a sound and complete Hoare logic for diverging programs This is joint work with @IlmariReissumies