1 Sofia University (BULGARIA)
2 Burgas Free University, Faculty of Computer Science and Engineering (BULGARIA)
About this paper:
Appears in: INTED2017 Proceedings
Publication year: 2017
Pages: 8195-8203
ISBN: 978-84-617-8491-2
ISSN: 2340-1079
doi: 10.21125/inted.2017.1930
Conference name: 11th International Technology, Education and Development Conference
Dates: 6-8 March, 2017
Location: Valencia, Spain
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.
Specification, Program Verification, Program Synthesis, Equivalence of Functions.