A team of researchers from the Massachusetts Institute of Technology (MIT), Cambridge, Massachusetts has developed a new programming language known as ‘A Tensor Language’ (ATL) written specifically for high-performance computing.
Amanda Liu, a second-year Ph.D. student at the MIT Computer Science and Artificial Intelligence Laboratory (CSAIL) commented:
… speed and correctness do not have to compete. Instead, they can go together, hand-in-hand, in the programs we write.
The language was introduced last month at the Principles of Programming Languages conference in Philadelphia.
Liu further stated:
Everything in our language is aimed at producing either a single number or a tensor … Given that high-performance computing is so resource-intensive, you want to be able to modify, or rewrite, programs into an optimal form to speed things up. One often starts with a program that is easiest to write, but that may not be the fastest way to run it so further adjustments are still needed. We can guarantee that this optimization is correct by using something called a proof assistant.
The team’s new language builds upon an existing language, Coq, that contains a proof assistant. The proof assistant has the inherent capacity to prove its assertions in a mathematically rigorous fashion. The team cautions that ATL is still a prototype, given that:
One of our main goals, looking ahead, is to improve the scalability of ATL, so that it can be used for the larger programs we see in the real world.
Liu concludes “people will be able to follow a much more principled approach to rewriting these programs — and do so with greater ease and greater assurance of correctness.”
