Industrial applications of software synthesis via category theory

Over the last two years, we have demonstrated the feasibility of applying category-theoretic methods in specifying, synthesizing, and maintaining industrial strength software systems. We have been using a first-of-its-kind tool for this purpose. Kestrel´s Specware^TM software development system. In this paper, we describe our experiences and give an industrial perspective on what is needed to make this technology have broader appeal to industry. Our overall impression is that the technology does work for industrial strength applications, but that it needs additional work to make it more usable. We believe this work marks a turning point in the use of mathematically rigorous approaches to industrial strength software development and maintenance. It is interesting to note that when this technology is applied to software systems whose outputs are designs for airplane parts, the design rationale that is captured is not only software engineering design rationale, but also design rationale from other engineering disciplines (e.g., mechanical, material, manufacturing, etc.). This suggests the technology provides an approach to general systems engineering that enables one to structure and reuse engineering knowledge broadly