I think you're wrong.  The only occurrence of /dev/std* in the source
is in a table that makes them work in awk programs.  That is,

awk 'BEGIN {print "hello world" >"/dev/stderr" }'

works because of that table.  It's not a bug.