The operator ==> binds weaker than && and ||, as is suggested by the fact that ==> is 3 characters wide, whereas the others are only 2 characters wide.

[...]

As you go through this book, I will not be surprised if you often forget that programs can be run -- most of your time will be spent specifying, writing, and proving the programs, and when the verifier finally has no more complaints, you know the program satisfies the specification (so why even run it, right? 😉).

-- Program Proofs