At Galois Connections, our business includes the construction of high-assurance software using formal methods. Our primary formal method is to program in modem functional programming languages, such as Haskell. These languages have powerful type systems that prevent certain classes of errors and promote intellectual control. Moreover, good functional programs have traits such as being declarative, using high levels of abstraction, using small, embedded domaln-specifin languages at appropriate points, and adopting a mathematical bias. We have found by experience that functional programming is a very effective industrial technique, one that lies in the "sweet spot" on the terrain that stretches between formal methods theory and induslrial practice.