Converting a Hardware description language to a functional programming language
You could write an interpreter for VHDL or Verilog in e.g. Coq or Isabelle/HOL and then prove that translated hardware descriptions do the right thing. I know that people have done this, at least for fragments of the hardware description languages, see e.g. A Formal Executable Semantics of Verilog.  Companies like Intel or AMD formally verify (parts of) the design of their chips. Have a look at Roope Kaivola's work.