Engineering software correctness

Software engineering courses offer one of many opportunities for providing students with a significant experience in declarative programming. This report discusses some results from taking advantage of this opportunity in a two-semester sequence of software engineering courses for students in their final year of baccalaureate studies in computer science. The sequence is based on functional programming using ACL2, a purely functional subset of Common Lisp with a built-in, computational logic developed by J Strother Moore and his colleagues over the past three decades. The course sequence has been offered twice, so far, in two consecutive academic years. Certain improvements evolved in the second offering, and while this report focuses on that offering, it also offers reasons for the changes. The discussion outlines the topical coverage and required projects, suggests further improvements, and observes educational effects based on conversations with students and evaluations of their course projects. In general, it appears that most students enjoyed the approach and learned concepts and practices of interest to them. Seventy-six students have completed the two-course sequence, half of them in the first offering and half in the second. All of the students gained enough competence in functional programming to apply it in future projects in industry or graduate school. In the second offering, about forty percent of the students gained enough competence with the ACL2 mechanized logic to make significant use of it in verifying properties of software. About ten percent acquired more competence than might reasonably be expected, enough to see new opportunities for applications and lead future software development efforts in the direction of declarative software with proven correctness properties.