I read that type checking is easier with dependent types. I'm barely aware of adga adn other langs that are used for profs, but wonder how useful (and what dan

I read that type checking is easier with dependent types. I'm barely aware of adga adn other langs that are used for profs, but wonder how useful (and what danger ahead) could cause to design a language with this for more mundane purposes (like, for example, build websites, data manipulation, gui, etc)