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