VERIFICATION AND SYNTHESIS OF PROGRAMS IN INTRODUCTORY COURSES IN FUNCTIONAL PROGRAMMING

The so called “polyglot programming” has been a paradigm gaining speed during the last decade. It requires the developers to employ the most suitable programming language depending on the particular task to be solved. This motivates the programmers to integrate languages realizing different programming styles in the program environments they develop.

The functional programming languages are among the most appropriate for a number of applications in the field of artificial intelligence, for execution of program prototypes with dynamic design, for scientific research, for studying program properties, etc. The declarative nature of these languages makes them suitable for expressing the laws and relations between the parts of the program, for modelling business rules, for applying as meta-languages, describing specifications and models, etc. This explains the emerging of a great number of contemporary languages of functional programming, as well as the programming language creators’ strife to integrate the functional style into the contemporary programming environments.

Responding to the practice needs, and in order to provide highly-trained specialists, the universities providing software engineer education increase the training in functional languages programming. In order to achieve this, formal methods through which to investigate program properties have been introduced in addition to the basic structures of the functional languages.

This article presents its authors’ experience in applying formal methods of verification and synthesis of functional programs, as well as of proving properties of functional programs, in introductory courses in functional programming. It analyzes the benefits and drawbacks of education through applying formal methods. Opportunities for improving the results of such type of education are discussed.

The work is based on Haskell and Scheme languages of functional programming.