Fractran

A few days ago a commenter here mentioned a proof by Conway that some Collatz-like sequences are undecidable.

A friend tracked down talk slides by Terry Tao (https://terrytao.files.wordpress.com/2020/02/collatz.pdf) where he gives the proof, in the form of a design of a turing complete esoteric programming language where a program is iteration of a formula of the shape "if n is divisible by m, n := an/b, else if n is divisible by ..., ..., else n := yn/z". Since this can be shown to be turing complete, some programs are undecidable.