I haven't used blues long enough to answer that question, but I would definitely say that the bump is not terribly pronounced. I have been away from my mechanical keyboard for about two months now (moving and no work) and I know when I get back to it I'll be bottoming out the keys every time. But it's enough so that once you get used to it you can use it properly and comfortably, which is the whole point.

The thing about the smaller boards is that they just feel more cramped, even if you actually have the same size keys—but that's obviously just personal preference.

For anyone who happens to read this and gets interested in Coq, I found that my understanding of the inner workings of it—and thus my ability to do proofs—was hugely aided by running (equivalently) "Show Proof." during proof-editing mode, or "Print <X>." where <X> is the proof object after it is defined.

Thus one learns that (forall n:nat, n + 0 = n) is inhabited by

   nat_ind (fun n => n + 0 = n)
           eq_refl
           (fun n0 IH => eq_ind_r (fun n1 => S n1 = S n0) eq_refl IH)
           n

I have two identical Leopold tenkeyless with Cherry MX Browns; one for home and one for work. Feels like blue switches, but with much less clicky-clicky.

As for the layout, it's compact without being squished like laptop keyboards, *shudder*. Arrow keys and the other navigation keys get their own space without being in the way.