Q# is a high-level programming language from Microsoft for writing and running quantum programs. Like most industrial languages, it was designed without a formal specification, which can naturally lead to ambiguity in its interpretation. We aim to provide a formal specification and semantics for Q#, placing the language on a solid mathematical foundation, enabling further evolution of its design and type system, and leading to research in program correctness and verified compiler implementation. This poster describes our current progress and outlines the next steps.
Extended abstract accepted to QPL 2021 for the Poster Session.