[Seanny123]

I don't understand type systems very well. When you say "check correctness" do you mean something beyond static linting with type-hints, like in Python? Or do you mean something deeper, like in functional languages like Elm and F#?

Also, is there always a trade-off between types and flexible meta-programming? Like, OCaml has meta-programming capabilities, but they make type-checking way harder, according to my PhD friend who's written extensively in Scheme and OCaml.