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 specif

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.