在上月於費城舉辦的編程語言原理大會上，麻省理工學院（MIT）計算機科學與人工智能實驗室（CSAIL）二年級博士生 Amanda Liu 表示，使用他們專為高性能計算而設計的新編程語言，可以很好地兼顧速度與正確性。此前人們普遍認為，速度與可靠性存在不可避免的權衡。
據悉，Liu 與加州大學伯克利分校博士后 Gilbert Louis Bernstein、MIT 副教授 Adam Chlipala 和助理教授 Jonathan Ragan-Kelley 一道，描述了他們最近開發的“張量語言”（A Tensor Language）。
ATL 語言旨在產生一個數字或張量，所謂張量就向向量和矩陣的泛化。
向量是一維對象（通常由單獨的箭頭表示），矩陣是相對臉熟的二維數字數組。
而張量是 n 維數組，例如可用 3×3×3 的數組形式、或更高 / 更低的維度。
a verified framework for optimizing tensor programs（via）
計算機算法或程序的全部意義，在於啟動特定的計算。不過想要實現目的，可用諸多不同的方式來編寫。正如該研究團隊在即將發表的會議論文中所寫的那樣：
各種不同的代碼實現方式讓人眼花繚亂，某些方案的速度要快得多。
但鑒於高性能計算的資源開銷極其誇張，ATL 希望用更高效的方式來修改或重寫程序。
普通開發者習慣從最容易着手的地方開始編程，但這顯然沒有考慮到最佳的運行效率，因而需要進一步調整優化。
假設圖像由 100×100 的數字數組表示，每個數字對應一個像素，且希望獲得這些數字的均值。
這項工作可通過兩階計算完成，首先確定每行的平均值，然後獲取每列的平均值。
ATL 提供了一個相關的工具包 —— 計算機科學家稱之為“框架”—— 能夠展示如何將這兩個步驟轉換為更快的一步過程。
Liu 補充道：我們可藉助所謂的“證明助手”（proof assistant），來確保這種優化的正確性。
有鑒於此，團隊在現有的 Coq 語言的基礎上構建了新語言。而其中包含的證明助手，具有以數學嚴謹的方式證明其斷言的內在能力。
不過在 MIT 團隊看來，Coq 有另一個值得稱道的內在特性 —— 用它編寫或適配的程序，是無法在無限循環中無止境地運行的。
舉個例子，用 Java 編寫的程序，可能會發生這種狀況。我們運行一個程序來得到一個單一的答案 —— 一個數字、或一個張量。
一個永不終止的程序，對我們說來毫無用處，但終止（terminate）是我們可使用 Coq 免費獲得的一項特性。
只得一提的是，ATL 項目結合了 Ragan-Kelley 和 Chlipala 兩項研究的成果，前者長期持續關注着高性能計算背景下的算法優化。
與此同時，Chlipala 更關注算法優化的形式化（例如基於數學的驗證），但 ATL 是兩者都首次合作 —— Bernstein 和 Liu 與去年攜手，併產出了 ATL 這個成果。
據悉，ATL 是首個、也是迄今唯一一個具有正式驗證優化的張量語言。目前 ATL 仍處於原型階段，但研究團隊已在許多小程序上展開了測試，可知其具有相當光明的前景。
展望未來，他們的主要目標之一是提升 ATL 的可擴展性，以便它能夠用於我們在現實世界中看到的更大型的程序。
此前這些程序的優化工作，通常需要人工來完成。除了總有臨時需要解決的問題、還總涉及反覆實驗，因而難免發生大量的錯誤。
好消息是，藉助 ATL，我們有望遵循一種更具原則的方法來重寫這些程序 —— 且這麼做更加容易，也更能保證程序的正確性。