Hoare Type Theory (HTT) is as a powerful tool for “structuring the verification of heap manipulating programs”: it complements higher-order dependently-typed systems like Coq with features for specification and verification of low-level stateful operations in the style of Hoare Logic. This talk presents an ongoing work triggered by the following question: what if the structure of the program is not so structured? Hoare-style reasoning about “jumpsy” programs is long known to be intricate, to say the least. Our approach to tackle this matter is to extend the HTT language with a control operator, callcc, similar to the one you would find in your favourite functional programming language. We will discuss our current implementation, some results, several pitfalls we have encountered, and a couple ideas for avoiding falling off the cliff.