Contemporary digital systems, with hundreds of thousands of gates to a chip (and large recall costs!), are a prime area for the application of formal methods.
I will give an overview of the use of higher-order logic for describing and reasoning about digital systems and then focus on the gains, and drawbacks, offered by the use of dependent types.