b'
GADTs are quite powerful.\\xa0 Why go all the way to true dependent types?\\xa0 And should you use the Curry-Howard isomorphism (see Chapter 3 of the podcast) or not?