MIT研究人员发展专用于高性能计算的程序语言ATL（A Tensor Language），该语言强调能够兼具性能与可靠性。ATL以程序语言Coq为基础，并且提供了证明助理，以验证ATL的优化正确无误。
现在越来越多的应用，像是机器学习与图片处理，皆需依赖高性能计算，人们普遍认为，在追求速度的同时，可能需要牺牲可靠性，而MIT研究人员则挑战了该观点，研究人员提到，速度和正确性可以不需要竞争，在ATL中可以同时实现。
由于高性能计算非常消耗资源，程序需要以优化的形式编写，来加快执行速度，但是开发人员通常以最容易的方式编写，因此都需要进一步调整。而ATL便能够在这种时候帮上忙，针对复杂的运算，ATL提供优化程序开发框架，可以将原本多步骤的运算过程，转换成较少的且较快的运算方法。
ATL创建在现有程序语言Coq之上，并提供了证明助理，该证明助理能以严谨的数学方法，证明优化的正确性，经证明助理验证过后的程序，能够确保最终仍可获得正确答案。
研究人员提到，过去程序的优化不少都要以手动进行，需要经过大量反复试错的过程，而ATL提供了更具规则的方式执行程序优化。ATL目前是唯一能够真正验证其优化的张量语言，目前还在初期研究阶段，研究人员正提高ATL的可扩展性，以便应用在现实中更大的程序中。