越来越多的任务需要高性能计算——例如图像处理或神经网络上的各种深度学习应用程序——在这些任务中，人们必须处理大量数据，并且速度相当快，否则可能会很荒谬时间。人们普遍认为，在执行此类操作时，在速度和可靠性之间存在不可避免的权衡。根据这种观点，如果速度是重中之重，那么可靠性可能会受到影响，反之亦然。
然而，主要位于麻省理工学院的一组研究人员对这一概念提出了质疑，声称事实上，一个人可以拥有一切。麻省理工学院计算机科学与人工智能实验室(CSAIL)的二年级博士生AmandaLiu说，使用他们专门为高性能计算编写的新编程语言，“速度和正确性不必竞争.相反，他们可以在我们编写的程序中携手并进。”
Liu与加州大学伯克利分校博士后GilbertLouisBernstein、麻省理工学院副教授AdamChlipala和麻省理工学院助理教授JonathanRagan-Kelley一起描述了他们最近开发的“张量语言”（ATL）的潜力，上个月在费城编程语言原则会议。
“我们语言中的一切，”刘说，“都是为了产生一个数字或一个张量。”反过来，张量是向量和矩阵的泛化。向量是一维对象（通常由单独的箭头表示），矩阵是熟悉的二维数字数组，而张量是n维数组，例如可以采用3x3x3数组的形式，或者更高的形式（或更低）尺寸。
计算机算法或程序的全部意义在于启动特定的计算。但是可以有许多不同的方式来编写这个程序——正如Liu和她的合著者在他们即将发表的会议论文中所写的那样，“各种不同的代码实现令人眼花缭乱”——有些方式比其他方式快得多。她解释说，ATL背后的主要理由是：“鉴于高性能计算非常耗费资源，您希望能够将程序修改或重写为最佳形式以加快速度。人们通常从最容易编写的程序开始，但这可能不是运行它的最快方式，因此仍需要进一步调整。”
例如，假设图像由×的数字数组表示，每个数字对应一个像素，并且您希望获得这些数字的平均值。这可以在两阶段计算中完成，首先确定每行的平均值，然后获取每列的平均值。ATL有一个相关的工具包——计算机科学家称之为“框架”——它可以展示如何将这个两步过程转换为更快的一步过程。
“我们可以通过使用一种叫做证明助手的东西来保证这种优化是正确的，”刘说。为此，团队的新语言建立在现有语言Coq的基础上，其中包含一个证明助手。反过来，证明助手具有以数学严谨的方式证明其断言的内在能力。
Coq有另一个内在特性使其对基于MIT的团队具有吸引力：用它编写的程序或其改编版总是终止并且不能在无限循环中永远运行（例如，用Java编写的程序可能会发生这种情况）。“我们运行一个程序来得到一个单一的答案——一个数字或一个张量，”刘坚持说。“一个永不终止的程序对我们来说毫无用处，但终止是我们通过使用Coq免费获得的东西。”
ATL项目结合了Ragan-Kelley和Chlipala的两个主要研究兴趣。Ragan-Kelley长期以来一直