There is not single angle where bb makes sense. I started rewriting it with chez scheme. I added checks, and property testing ala quick check. Here is an example use:

There is two ways to compare a tiered leaderboard first tier get first, then within the tier it is ranked by score with max 1000.

So the function looks like:

(lambda (tier1 score1 tier2 score2)
(if (< tier1 tier2) #true
(if (= tier1 tier2) (< score1 score2)
#false)))

But there is faster way to do the “same” thing with a single comparison:

(define pack (lambda (tier score) (+ (* tier 1000) score)))

(lambda (tier1 score1 tier2 score2)
(< (pack tier1 score1) (pack tier2 score2)))

The packing trick only works when scores fit in the multiplier's range. If score >= 1000, the packed value bleeds into the next tier: tier=1, score=1001 packs to 2001, which beats tier=2, score=0 at 2000 — wrong, because tier 2 should always win.

Adding the following check to bb, surface the bug:

cat <<'EOF' | bb add -
;; Without bounds, the packing trick fails.
(define ~check-unbounded-equivalence
(lambda (f)
(lambda (t1 s1 t2 s2)
(assume (= (f t1 s1 t2 s2)
(slow-compare t1 s1 t2 s2))))))
EOF
bb add --check fast-compare unbounded-equivalence
bb check fast-compare 2>&1 | grep Z3-FAIL

Mind the fact that it looks like regular #scheme