They seem to operate at much higher level of abstraction. They mean something more profound when they speak of "types", which I don't understand. Also Ada seems interesting, with more spelled out contracts.
That depends on the types. You can have something as basic as "int", something a bit more complex like arrays, or something even more complex like GADTs https://v2.ocaml.org/manual/gadts.html
