I would say no.

Type-checking for many popular programming languages (e.g. Java, C++, C#, Rust, OCaml, Scala, Swift) is undecidable, and for practical purposes this fact is little more than a curiosity.
The question of whether, given a finite POMDP, any policy exists that achieves at least zero expected reward is undecidable, and for practical RL this is not even much of a curiosity.
Any function from that is well-defined is computable, because there exists a finite encoding of a lookup table. No Myhill–Nerode needed.
I think a more compelling formalization of the Busy Beaver problem's hardness is that for $i \geq 748$ , the value of $B B (i)$ is independent of ZF set theory. In some sense $B B (748)$ alone is uncomputable, even though it's just a single natural number rather than a function that has to work for infinitely many inputs.