The syntax is a monstrosity. You can also extract a proven OCaml program from Coq and Coq has a beautiful syntax.

If you insist on the same language for specifying types, some Lisp variants do that with a much nicer syntax.

Python people have been indoctrinated since ctypes that a monstrous type syntax is normal and they reject anything else. In fact Python type hints are basically stuck on the ctypes level syntax wise.