MIT researches develop new programming language designed for high-performance computing

A team of researchers from the Massachusetts Institute of Technology (MIT) has developed a new programming language known as “A Tensor Language” (ATL) designed for high-performance computing that could solve the issue of trade-offs between speed and reliability. 

The ATL team includes Gilbert Louis Bernstein, a postdoc at the University of California at Berkeley, MIT Associate Professor Adam Chlipala, MIT Assistant Professor Jonathan Ragan-Kelley, and Amanda Liu, a second-year Ph.D. student at the MIT Computer Science and Artificial Intelligence Laboratory (CSAIL). In speaking about their development, they said their creation can offer speed and correctness together in the programs they write. 

According to a report from MIT News, the programming language is focused on producing either a single number or a tensor, which is a generalization of vectors and matrices. Liu explained that the primary goal behind ATL is to modify or rewrite programs into an optimal form to speed things up. The team’s new language builds upon an existing language called Coq which contains a proof assistant. This feature allows ATL to mathematically prove its assertions and guarantees that the optimization is correct.

Programs written in Coq, or adaptations of it, always terminate and cannot run on endless loops like programs written in Java, the report states. This made them more attractive to the MIT-based team as they said a program that never terminates would be useless to them. 

“We run a program to get a single answer — a number or a tensor,” Liu told MIT News. “A program that never terminates would be useless to us, but termination is something we get for free by making use of Coq.”

The ATL project combines two of the main research interests of Ragan-Kelley and Chlipala, marking their first collaboration. While Ragan-Kelley has long been concerned with the optimization of algorithms in the context of high-performance computing, Chlipala has focused more on the formal verification of algorithmic optimizations. According to the report, the team’s new creation is the first, and so far the only, tensor language with formally verified optimizations. It has been tested on small programs and is still a prototype. However, it is a promising one that has the potential to scale up and be used for larger programs in the real world.

The optimization of programs in the past has typically been done by hand on an ad hoc basis, which often involves trial and error. ATL could change this as it allows people to follow a more principled approach to rewriting these programs with greater ease and greater assurance of correctness, the report states. The potential of ATL was presented at the Principles of Programming Languages conference in Philadelphia last month. According to the report, the team is now focused on improving the scalability of ATL so that it can be used for larger programs. The programming language could be a game-changer in the field of high-performance computing. Its ability to provide speed and correctness together in programs could have significant implications for image processing and various deep-learning applications on neural nets.