Yes. For instance, say you&#x27;re implementing a red-black tree. In case your algorithms are as rusty as mine are: it&#x27;s a particular form of binary tree where every node has a &quot;color&quot;, red or black, the children of any red node are black, all leaves are black, and the count of black nodes from the root to any leaf (aka the &quot;black-height&quot;) is the same. The intention is that the tree is roughly balanced by following these rules: the minimum height is the black-height (all black nodes), and the maximum height is double the black-height (alternating red and black).<p>You might want to check that the property &quot;the number of black nodes from the root to any leaf is the same&quot; is always valid. With unit testing, you&#x27;d implement the insertion and deletion functions, and write a unit test where you give them a few trees and make sure that the insertion and deletion functions don&#x27;t break that property, probably by looping over every leaf and comparing the black-height. If this passes, you know that your functions are probably correct and at least not <i>obviously</i> broken, but you don&#x27;t know that there isn&#x27;t some edge case you haven&#x27;t thought of.<p>With a language that supports proofs, you&#x27;d tell the compiler about the concept of black-height, and the type of a red-black tree would include the black-height. Therefore, in order to construct a valid red-black tree, you have to have constant black-height. Just as much as you couldn&#x27;t construct a red node with a red child, you can&#x27;t construct a node with two children of varying black-height. When you say that your insertion function returns a red-black tree, as part of type-checking, the compiler makes sure that these properties hold -- because in turn, every helper function you call, every constructor, etc. also requires these properties to hold so that they can return an object of type red-black tree.<p>The downside is that it&#x27;s <i>much</i> more involved than a few randomly-selected test cases to convince the compiler that you&#x27;re upholding the red-black tree rules in every single case. This textbook has an example of doing this in the Coq proof assistant (search for the section labeled &quot;Dependently Typed Red-Black Trees&quot;):<p><a href="http:&#x2F;&#x2F;adam.chlipala.net&#x2F;cpdt&#x2F;html&#x2F;MoreDep.html" rel="nofollow">http:&#x2F;&#x2F;adam.chlipala.net&#x2F;cpdt&#x2F;html&#x2F;MoreDep.html</a>