This is why they brought up the language that uses the same syntax for types as it does for your function definition. It really sounds like you haven't played

This is why they brought up the language that uses the same syntax for types as it does for your function definition. It really sounds like you haven't played with Coq or Agda.. because expressing these things are not that much code at all. Also the presentation literally covers that complaint, and how they think more programming languages are needed.