麻省理工学院正在为高性能计算机开发一种新的编程语言

需要高性能计算来解决越来越多的任务——例如图像处理或神经网络上的各种深度学习应用——你需要处理大量数据，并且处理得足够快，否则可能需要大量的时间时间。 人们普遍认为，在执行此类操作时，速度和可靠性之间的折衷是不可避免的。 根据这种想法，如果优先考虑速度，那么可靠性可能会受到影响，反之亦然。

然而，主要位于麻省理工学院 (MIT) 的一组研究人员正在挑战这一概念，认为你实际上可以拥有一切。 根据麻省理工学院计算机科学与人工智能实验室 (CSAIL) 的二年级研究生 Amanda Liu 的说法，他们使用一种专门为高性能计算编写的新编程语言，“速度和正确性不必竞争。 相反，在我们编写的程序中，它们可以并肩并肩。” Liu 和她的团队上个月在费城举行的编程语言原理会议上谈到了他们新创建的 A Tensor Language (ATL) 的潜力。

“我们语言中的一切，”刘说，“旨在获得一个数字或一个张量。” 反过来，张量是向量和矩阵的推广。 向量是一维对象（通常用单个箭头表示），矩阵是常见的二维数字数组，而张量是 n 维数组，可以采用 3×3×3 数组的形式，例如，甚至更高（或更低）的维度。

计算机算法或程序的本质是发起某种计算。 但是可以有许多不同的方法来编写这个程序——“令人惊讶的各种不同的代码实现”，正如 Liu 和她的合著者在他们的论文中所写的那样——其中一些方法比其他方法快得多。 她解释说，ATL 背后的主要理由是：“鉴于高性能计算是如此耗费资源，您希望能够以最佳形式修改或重写程序以加快速度。 通常你会从最容易编写的程序开始，但这可能不是运行它的最快方法，所以你仍然需要做进一步的调整。”

新的命令语言基于现有的 Coq 语言，其中包括一个证明助手。 反过来，证明助手有能力在数学上精确地证明其陈述。 Coq 还有另一个吸引 MIT 小组的特性：用这种语言编写的程序，或者它的改编版，总是终止并且不能在无限循环中无限期地运行。

现在它是第一个也是迄今为止唯一一个经过形式验证优化的张量语言。 然而，麻省理工学院的团队警告说，ATL 仍然只是一个原型——尽管是一个很有前途的原型——已经在许多小程序上进行了测试。

另请阅读：

• 为正确的 Windows 更新命名条件
• OpenAI 教人工智能将命令转换为程序代码