Question about the intended semantics for inline `#:` type assertions on local variables

[infiton]

Now that inline RBS comments are in ruby/rbs I'd like to clarify what the #: type assertion on a local variable is supposed to mean and to make sure that we aren't baking in a semantic difference between steep and sorbet.

For instance in the following code:

x = "hi" #: String
x = 5

• Steep (verified on 2.0.0) treats #: as a type assertion on the expression (introduced in Steep 1.3 as "declaring the type of an expression inline, without introducing a new local variable with a @type var annotation"). The local remains flow-typed, so the later x = 5 re-infers x to Integer — no error at the reassignment.
• Sorbet (verified on 0.6.13327 (RBS comments support) lowers x = v #: T to x = T.let(v, T). T.let declares the local's type for the whole method scope, so x = 5 is an error ("Incompatible assignment to variable declared via let").

This is extra confusing because in the case of

class Foo
  attr_accessor :bar #: String?
end

foo = Foo.new
Foo.bar = 5

results in an error in both Steep and Sorbet.

Questions

1. Is the semantics of a #: assertion on a local variable intended to be an expression-level assertion (Steep's behavior), a scope-level declaration/pin (Sorbet's T.let behavior), or is it deliberately left to each checker?
2. If it's left to checkers by design, can we consider documenting that (e.g. in docs/) so tool authors and users know portability is not guaranteed here?
3. If a single intended meaning is desired, is there a preference — and would it be worth a note in the inline-syntax docs so Steep/Sorbet/other implementations (RubyMine, and third-party checkers) can converge?