An explanation of why ACL2 has an explicit brr mode
Why isn't brr mode automatically disabled when there are no monitored runes? The reason is that the list of monitored runes is kept in a wormhole state.
See wormhole for more information on wormholes in general. But the
fundamental property of the wormhole function is that it is a logical
Break-rewrite interacts with the user in a wormhole state because the signature of the ACL2 rewrite function does not permit it to modify state. Hence, only wormhole interaction is possible. (This has the additional desirable property that the correctness of the rewriter does not depend on what the user does during interactive breaks within it; indeed, it is logically impossible for the user to affect the course of rewrite.)
Now consider the list of monitored runes. Is that kept in the external state as a normal state global or is it kept in the wormhole state? If it is in the external state then it can be inspected within the wormhole but not changed. This is unacceptable; it is common to change the monitored rules as the proof attempt progresses, installing monitors when certain rules are about to be used in certain contexts. Thus, the list of monitored runes must be kept as a wormhole variable. Hence, its value cannot be determined outside the wormhole, where the proof attempt is ongoing.
This raises another question: If the list of monitored runes is unknown to the rewriter operating on the external state, how does the rewriter know when to break? The answer is simple: it breaks every time, for every rune, if brr mode is enabled. The wormhole is entered (silently), computations are done within the wormhole state to determine if the user wants to see the break, and if so, interactions begin. For unmonitored runes and runes with false break conditions, the silent wormhole entry is followed by a silent wormhole exit and the user perceives no break.
Thus, the penalty for running with brr mode enabled when there are
no monitored runes is high: a wormhole is entered on every application of
every rune and the user is simply unaware of it. The user who has finally
unmonitored all runes is therefore strongly advised to carry this information
out of the wormhole and to do