在《科学》杂志发布的十大科学突破中，量子霸权赫然在列。但是，大众要想真正用上量子计算机，还需要具备实用功能的程序落地，需要触手可及的量子应用。 “众所周知，软件是计算机的‘灵魂’，一旦量子计算机研制成功，量子软件的开发将成为真正发挥量子计算机作用的关键。”中国科学院软件研究所学术副所长应明生说。 近日，中科院软件所及其合作团队正式发布了国内首个量子程序设计平台isQ，为量子程序设计提供“指南”，为批量验证提供平台的程序。 量子计算需要一个合适的新语境，经典的编程语境已经不适合了。与经典世界相比，量子系统具有许多完全不同的特性，如量子信息的不可克隆性、量子纠缠的非局域效应等，经典软件理论、方法和技术在很大程度上不能直接适用于量子软件. 微软的专利是通过模拟器将经典程序的调试方法“嫁接”到微量子程序的调试中。它的优点是可以直接利用已有的手段和方法。程序。 基于对量子语言的充分理解，isQ平台自带的编译器可以先将高级语言编写的量子程序转换成指令集语言，再交给后续工具进行进一步处理.该平台将帮助程序开发者轻松编写出更符合程序员思维的高级语言程序，并准确地转换成量子计算机能够理解的指令集语言。相关研究人员表示，该平台未来可以根据不同的硬件，转换成不同的指令集，实现对各种量子计算机的兼容。 量子计算语言给出指令的准确性取决于人类与量子世界“沟通”的程度。 程序纠错和正确性验证是量子计算的重要组成部分。目前量子程序的规模还比较小，也可以人工完成。比如写个两三百行或者几千行的代码，手工逐行查错。但是如果代码量达到几万甚至几十万行，人工验证就失效了。 因为量子程序与传统的计算机程序有很大的不同，尤其是由于量子叠加和纠缠的存在，量子程序的验证往往非常困难。 isQ中包含的定理证明器是世界上第一个能够验证大规模量子程序正确性的工具。 “它的实现是基于团队提出的量子霍尔逻辑。中科院软件所量子软件研究团队副研究员应盛刚表示，该工具是具有自主知识产权的成果，可以克服经典计算机计算时间和存储空间的限制，为更大规模的量子程序设计提供重要帮助。 具体来说就是通过参数化实现逻辑层面的验证，而不需要在系统中实际进行数值计算。因此，当量子比特数超过目前传统计算机模拟计算的极限时，这种方法也能够进行程序验证。使用定理证明器，普通的笔记本电脑也可以验证大规模量子程序的正确性，这是无法做到的由传统的超级计算机通过模拟器操作来完成。
