Description

The colon equals operator has special semantics and is used for assignment.

Equality is related to assignment, so after you execute
   a := b
by convention the following assertion should hold
   ~a == b

Semantics

The form
   a := b
is equivalent to
   Assign(a,b)

The form
   a ==#c b
is equivalent to
   c.sys:Eq(a,b)