The unique features of the hybrid quantum-classical computing model implied by the specification of OpenQASM 3.0 motivate new approaches to quantum program verification. We implement a typed QASM 3.0 parser in TypeScript to enable implementations of verification and validation software, compilers and more. We also propose that a formal treatment of OpenQASM 3.0's type system in type theory notation may further facilitate formal verification. We highlight advancements in hybrid quantum-classical computing since the Quantum Hoare Logic to this end.

翻译：OpenQASM 3.0规范所蕴含的混合量子-经典计算模型的独特特性，推动了量子程序验证新方法的发展。我们基于TypeScript实现了一个类型化的QASM 3.0解析器，以支持验证与确认软件、编译器及其他工具的构建。我们进一步提出，采用类型理论符号对OpenQASM 3.0类型系统进行形式化处理，可进一步促进形式化验证的实现。为此，我们重点梳理了自量子霍尔逻辑提出以来混合量子-经典计算领域的最新进展。