Bidirectional transformation systems usually have a more declarative design, but it has long been realised that declarative approaches are hardly enough for practical bidirectional applications. The BX community currently concentrates on the exploration of more forms of well-behavedness laws, but we should not be satisfied with only well-behavedness guarantees. Instead, we should also start aiming to precisely reason about the behaviour of bidirectional programs like what we have been doing for general-purpose languages, and only then can we think about more complex bidirectional applications and the verification of their consistency restoration behaviour. We will talk about the Hoare-style logic recently presented at POPL 2018 for our putback-based bidirectional language BiGUL (for programming state-based asymmetric lenses), and discuss this direction with the community.