Some quotes from: Teach Foundational Language Principles, By Thomas Ball, Benjamin Zorn Communications of the ACM, Vol. 58 No. 5, Pages 30-31, 10.1145/2663342, May 2015.

The need for more people to learn to program has received widespread attention recently (see, for example, www.code.org and its recent “Hour of Code” held during CS Education week in December of 2013 and 2014). While the ability to program has tremendous potential to support and channel the creative power of people, we should remember that programming languages continuously arise as the need to solve new problems emerges and that it is language principles that are lasting. As we discuss in this Viewpoint, language foundations serve an increasingly important and necessary role in the design and implementation of complex software systems in use by industry. Industry needs more people educated in language principles to help it deliver reliable and efficient software solutions to its customers. ….

Experiences with bugs like the recent TLS heartbeat buffer read overrun in OpenSSL (Heartbleed) show the cost to companies and society of building fundamental infrastructure in dated programming languages with weak type systems (the C language in this case) that do not protect their abstractions. Several companies have developed new safe systems programming languages to address the challenge of programming scalable and reliable systems. … Such languages raise the level of programming via new type systems that provide more guarantees about the safety of program execution. ….

Our recommendations are three-fold, visiting the three topics discussed in this Viewpoint in reverse order (formal design languages, domain-specific languages, and new general-purpose programming languages).

First, computer science majors, many of whom will be the designers and implementers of next-generation systems, should get a grounding in logic, its application in design formalisms, and experience the creation and debugging of formal specifications with automated tools such as Alloy or TLA+. As Leslie Lamport says, “To designers of complex systems, the need for formal specs should be as obvious as the need for blueprints of a skyscraper. “The methods, tools, and materials for educating students about “formal specs” are ready for prime time.

Mechanisms such as “design by contract,” now available in mainstream programming languages, should be taught as part of introductory programming, as is done in the introductory programming language sequence at Carnegie Mellon University.

Students who learn the benefits of principled thinking and see the value of the related tools will retain these lessons throughout their careers. We are failing our computer science majors if we do not teach them about the value of formal specifications.

Authors Thomas Ball (tball@microsoft.com) is a principal researcher and co-manager of the Research in Software Engineering (RiSE) group at Microsoft Research, Redmond, WA.

Benjamin Zorn (zorn@microsoft.com) is a principal researcher and co-manager of the Research in Software Engineering (RiSE) group at Microsoft Research, Redmond, WA.