上个月在费城举行的编程语言原理会议上，麻省理工学院计算机科学与人工智能实验室（CSAIL）的二年级博士生阿曼达，使用他们新的编程语言是专为高性能计算而设计的，刘说它在速度和正确性之间提供了很好的平衡。以前人们普遍认为，速度和可靠性之间存在不可避免的权衡。Liu与加州大学伯克利分校博士后GilbertLouisBernstein、麻省理工学院副教授AdamChlipala和助理教授JonathanRagan-Kelley一起描述了他们最近开发的“张量语言”。ATL语言旨在产生数字或张量，这是向量和矩阵的概括。向量是一维对象（通常用单个箭头表示），而矩阵是相对熟悉的二维数字数组。张量是n维数组，例如3×3×3数组，或更高/更低的维度。计算机算法或程序的全部意义在于启动特定计算。但要达到目的，可以有多种不同的写法。正如研究团队在即将发表的会议论文中所写的那样，有一系列令人眼花缭乱的不同代码实现，其中一些速度要快得多。但鉴于高性能计算极其夸张的资源开销，ATL希望以更高效的方式修改或重写程序。普通开发者习惯于从最容易的地方开始编程，但这显然没有考虑到最佳的运行效率，因此需要进一步的调整和优化。假设一幅图像由100x100的数字数组表示，每个像素一个，您想要获取这些数字的平均值。这可以在两阶段计算中完成，首先确定每行的平均值，然后取每列的平均值。ATL提供了一个相关的工具包——计算机科学家称之为“框架”——可以展示如何将这两个步骤转换为更快的一步过程。刘补充说：我们可以借助所谓的“证明助手”来确保这种优化的正确性。考虑到这一点，该团队在现有的Coq语言之上构建了新语言。并且其中包含的证明助手具有以数学上严格的方式证明其断言的内在能力。不过在MIT团队看来，Coq还有另一个值得称赞的内在特性——用它编写或改编的程序不能无限循环地无限运行。例如，用Java编写的程序可能会发生这种情况。我们运行一个程序来获得一个单一的答案——一个数字，或者一个张量。永不终止的程序对我们来说是无用的，但终止是我们通过Coq免费获得的一项功能。唯一值得一提的是，ATL项目结合了Ragan-Kelley和Chlipala的两项研究成果。前者长期以来一直关注高性能计算背景下的算法优化。同时，Chlipala更关注算法优化的形式化（比如基于数学的验证），但ATL是两者的首次合作——Bernstein和Liu去年联手制作了ATL。据悉，ATL是第一个也是迄今为止唯一具有形式化验证优化的张量语言。ATL目前还处于原型阶段，但研究团队已经在很多小程序上对其进行了测试，可见其前景十分广阔。展望未来，他们的主要目标之一是提高ATL的可扩展性，以便它可以用于我们在现实世界中看到的更大的程序。以前，这些程序的优化通常需要手动操作。除了总是有临时问题需要解决这一事实外，总是涉及反复试验，因此必然会发生很多错误。好消息是，有了ATL，我们有望遵循更有原则的方法来重写这些程序——而且这样做更容易，也更有保证是正确的。
