bindology.red

.

@x8x I can't answer all the questions, as I don't know the implementation internals of Red, but I think you are correct on first point.
About the third point, I think it is because the a resulting from loading the string is bound to default global context. I may hypothesize that a-s in function's body are bound to local context at definition time, but loading happens in runtime, and a resulting from loading in runtime is not bound to functions context.

BTW, in my first snippet bind isn't needed actually, because a is bound in this case:

f: func [/local a][a: context [b: context [c: 'ok]] print do [a/b/c]] f
; or 
f: func [/local a][a: context [b: context [c: 'ok]] print reduce 'a/b/c] f
; or
f: func [/local a][a: context [b: context [c: 'ok]] print a/b/c] f
ok