在《科學》雜誌公佈的十大科學突破中，量子霸權赫然在列。但公眾想要真正用上量子計算機，還需要有實際功能的程序落地，需要觸手可及的量子APP。
    “眾所周知, 軟件是計算機的‘靈魂’。一旦量子計算機研製成功, 量子軟件的開發將變成真正發揮量子計算機作用的關鍵。”中科院軟件所學術副所長應明生表示。
    近日，中國科學院軟件研究所及合作團隊正式發佈了國內首個量子程序設計平台——isQ，為量子程序的設計給出“指南”，為程序批量驗證提供平台。
    量子計算需要一種適宜的新語境，經典編程語境不再適宜。由於量子系統與經典世界相比有許多完全不同的特徵，如量子信息的不可克隆性、量子糾纏的非局域作用等。經典的軟件理論、方法和技術在很大程度上不能直接適用於量子軟件。
    微軟的一個專利是通過模擬器將經典程序調試的方法“嫁接”到微型量子程序的調試，其優點是能直接利用已有的手段、方法，缺點是只能針對規模較小的量子程序。
    基於對量子語言的充分理解，isQ平台包含的編譯器能首先將高級語言編寫的量子程序轉化為指令集語言，然後交由後續工具進一步處理。平台將幫助程序開發者方便地編寫比較符合程式設計師思維的高級語言程序，並準確地轉換為量子計算機能理解的指令集語言。相關研究人員表示，平台未來可依據不同的硬件，轉換為不同的指令集，實現對多種量子計算機的兼容。
    量子計算語言所下達的指令是否準確，取決於人類與量子世界的“溝通”程度。
    程序的糾錯與正確性驗證，是量子計算的重要組成部分。目前量子程序規模還比較小，還可以通過人工的方式去完成，比如說寫個兩三百行、上千行的代碼，人工一行一行去檢查錯誤。但如果代碼量達到幾萬行甚至十幾萬行，人工驗證就失效了。
    由於量子程序與傳統電腦程式相比具有很大的不同, 特別是由於量子疊加和糾纏的存在, 量子程序的驗證往往非常困難。
    isQ中包含的定理證明器，是世界上首個能夠對大型量子程序是否正確進行驗證的工具。
    “它的實現基於團隊提出的量子霍爾邏輯。” 中科院軟件所量子軟件研究團隊副研究員應聖鋼說，該工具是自主知識產權的成果，可在經典計算機上克服計算時間與存儲空間的限制，為較大規模量子程序的設計提供重要幫助。
    具體地說，是通過參數化的方式實現邏輯層面的驗證，而不需要真正地在系統中進行數值運算。因此當量子比特數超過目前傳統計算機的模擬運算極限時，這一方法也能夠進行程序的驗證。利用定理證明器，一台普通的筆記本電腦也能進行大型量子程序的正確性驗證，這是傳統超級計算機通過模擬器運算無法完成的。