Position Statement

Logic-Based Program Synthesis: State of the Art and Future Trends

Volume

Papers from the 2002 AAAI Spring Symposium

Contents

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.