越來越多的任務需要高效能計算——例如影象處理或神經網路上的各種深度學習應用程式——在這些任務中，人們必須處理大量資料，並且速度相當快，否則可能會很荒謬時間。人們普遍認為，在執行此類操作時，在速度和可靠性之間存在不可避免的權衡。根據這種觀點，如果速度是重中之重，那麼可靠性可能會受到影響，反之亦然。
然而，主要位於麻省理工學院的一組研究人員對這一概念提出了質疑，聲稱事實上，一個人可以擁有一切。麻省理工學院計算機科學與人工智慧實驗室 (CSAIL) 的二年級博士生 Amanda Liu 說，使用他們專門為高效能計算編寫的新程式語言，“速度和正確性不必競爭. 相反，他們可以在我們編寫的程式中攜手並進。”
Liu 與加州大學伯克利分校博士後 Gilbert Louis Bernstein、麻省理工學院副教授 Adam Chlipala 和麻省理工學院助理教授 Jonathan Ragan-Kelley 一起描述了他們最近開發的“張量語言”（ATL）的潛力，上個月在費城程式語言原則會議。
“我們語言中的一切，”劉說，“都是為了產生一個數字或一個張量。” 反過來，張量是向量和矩陣的泛化。向量是一維物件（通常由單獨的箭頭表示），矩陣是熟悉的二維數字陣列，而張量是n維陣列，例如可以採用 3x3x3 陣列的形式，或者更高的形式（或更低）尺寸。
計算機演算法或程式的全部意義在於啟動特定的計算。但是可以有許多不同的方式來編寫這個程式——正如 Liu 和她的合著者在他們即將發表的會議論文中所寫的那樣，“各種不同的程式碼實現令人眼花繚亂”——有些方式比其他方式快得多。她解釋說，ATL 背後的主要理由是：“鑑於高效能計算非常耗費資源，您希望能夠將程式修改或重寫為最佳形式以加快速度。人們通常從最容易編寫的程式開始，但這可能不是執行它的最快方式，因此仍需要進一步調整。”
例如，假設影象由 100×100 的數字陣列表示，每個數字對應一個畫素，並且您希望獲得這些數字的平均值。這可以在兩階段計算中完成，首先確定每行的平均值，然後獲取每列的平均值。ATL 有一個相關的工具包——計算機科學家稱之為“框架”——它可以展示如何將這個兩步過程轉換為更快的一步過程。
“我們可以透過使用一種叫做證明助手的東西來保證這種最佳化是正確的，”劉說。為此，團隊的新語言建立在現有語言 Coq 的基礎上，其中包含一個證明助手。反過來，證明助手具有以數學嚴謹的方式證明其斷言的內在能力。
Coq 有另一個內在特性使其對基於 MIT 的團隊具有吸引力：用它編寫的程式或其改編版總是終止並且不能在無限迴圈中永遠執行（例如，用 Java 編寫的程式可能會發生這種情況）。“我們執行一個程式來得到一個單一的答案——一個數字或一個張量，”劉堅持說。“一個永不終止的程式對我們來說毫無用處，但終止是我們透過使用 Coq 免費獲得的東西。”
ATL 專案結合了 Ragan-Kelley 和 Chlipala 的兩個主要研究興趣。Ragan-Kelley 長期以來一直關注高效能計算背景下的演算法最佳化。與此同時，Chlipala 更關注演算法最佳化的形式化（如基於數學的）驗證。這代表了他們的第一次合作。Bernstein 和 Liu 去年被引入企業，ATL 就是結果。
它現在是第一個，也是迄今為止唯一一個具有正式驗證最佳化的張量語言。然而，Liu 告誡說，ATL 仍然只是一個原型——儘管它很有希望——它已經在許多小程式上進行了測試。“展望未來，我們的主要目標之一是提高 ATL 的可擴充套件性，以便它可以用於我們在現實世界中看到的更大的程式，”她說。
過去，這些程式的最佳化通常是手工完成的，而且更加臨時，這通常涉及反覆試驗，有時還會出現大量錯誤。使用 ATL，Liu 補充說，“人們將能夠遵循一種更有原則的方法來重寫這些程式——而且這樣做更容易，也更能保證正確性。”
