Computer programs abound in our lives, embedded in a variety of equipment and devices such as electric appliances, PCs, mobile phones, and gaming devices.
To make our lives more convenient, computer programs tend to become large and complex unless the developers are careful enough to structure the code in a principled way. It is not uncommon for computer programs to be more than one million lines of code, and the inconsistency of a program may compromise the performance, functionality, and reliability of the whole information system. Research Unit on Theory and Practice of Programming aims at developing the highly reliable computer programs. Our slogan is “Correct programs are simple and beautiful”.

Programming as a scientific discipline

     Computer programs are considered large and complex. However, simpler and more applicable programs can be developed by incorporating mathematics into them. The most important issue for software is its correctness, or assured reliability. However, reliability alone does not make sense. For example, a traffic signal is guaranteed to be safe, if it is always red (“don’t go”), but this safety is meaningless, and we want to have a traffic signal which allows maximal traffic while ensuring its safety. Similarly, our goal is to develop highly reliable, highly functioning, and high performant programs, and the research unit conducts scientific research on programming, using scientific and systematic approaches. Our research activities also include program transformation, program synthesis, and program verification.

Figure 1: Requirements to software

Building systems that verify programs

     Current computer programs are becoming increasingly larger and more complex, partly because specialized development has been done to address their users’ divergent requests. Often many different versions of a single software are developed for different types of hardware. This is not only inconvenient from the perspective of maintenance, but it may also reduce the reliability of programs. To solve these problems, the research unit focuses on multi-stage programing (MSP), in which we write a code-generator, which, when executed, generates code specialized in specific domain or hardware, and then the generated code is executed to produce the final results. Previous studies could not establish the reliability of MSP-based programs with computational effects,*1 which are essential for the efficiency of the generated code The problem remained open for more than ten years, and for the first time in the world, we have developed a method for establishing the reliability of multi-stage programs with computational effects. The research unit continues the efforts to enhance the reliability of programs based on scientific approaches.

Figure 2: Concepts of multi-stage programming

*1: Computational effect is a feature of programs such as updating the values of variables and the input/output operations to a file. While works in the literature only targeted programs without computational effects, they are indispensable to generate efficient code without duplication.

(Interviewed on October 23, 2013)