在上月于費城舉辦的程式設計語言原理大會上，麻省理工學院（MIT）計算機科學與人工智能實驗室（CSAIL）二年級博士生 Amanda Liu 表示，使用他們專為高性能計算而設計的新程式設計語言，可以很好地兼顧速度與正确性。此前人們普遍認為，速度與可靠性存在不可避免的權衡。
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，我們有望遵循一種更具原則的方法來重寫這些程式 —— 且這麼做更加容易，也更能保證程式的正确性。