I disagree with the fact that types are moving over to the right side for readability's sake or anything like that. Modern theorem proving languages explicitly

I disagree with the fact that types are moving over to the right side for readability's sake or anything like that. Modern theorem proving languages explicitly specify that type declarations are simply equivalent to set inclusion, which makes the type specification operator (usually :) equivalent to set inclusion (∈). This influence was what rubbed off onto modern MLs, and by extension, inspired many of the ML inspired/type safe languages that have come out recently.