Just as abstract blocks, "white-box blocks" are program expressions
with an additional contract attached to their execution place.
Contrary to abstract blocks, whiteboxes do not hide their contents
from the outer computation. In most cases, you would not need
whiteboxes at all, as the same effect can be achieved by adding
assertions. Their utility comes from their syntax: the added
contract clauses bind to the expression and do not require
additional semicolons, begin-end's, let-in's or try-with's.

Compare:

    let x = <expr> in assert { P x }; x
to  <expr> ensures { P result }
or  <expr> returns { x -> P x }

    if ... then begin let x = <expr> in assert { P x }; x end; ...
to  if ... then <expr> ensures { P result }; ...

    try <expr> with E x -> assert { P x }; raise E x; end
to  <expr> raises { E x -> P x }

Internally, whiteboxes are just abstract blocks (zero-argument
anonymous functions executed in-place) with the label "vc:white_box"
on top. The user never needs to write this label explicitly though.