Actually it&#x27;s not that easy. Everywhere you have a type you need to proof that the expression really has the right type, and it&#x27;s not just type annotation, it&#x27;s a real mathematical proof.<p>To understand the complexity of the task, try proving that insertion sort is really a sort algorithm. You write more code, and writing it will take more time than you would do in a &#x27;normal&#x27; typed language.