While the realization of scalable quantum computation will arguably require topological stabilization and, with it, topological-hardware-aware quantum programming and topological-quantum circuit verification, the proper combination of these strategies into dedicated it topological quantum programming languages has not yet received attention.

Here we describe a fundamental and natural scheme that we are developing, for typed functional (hence verifiable) topological quantum programming which is topological-hardware aware – in that it natively reflects the universal fine technical detail of topological q-bits, namely of symmetry-protected (or enhanced) topologically ordered Laughlin-type anyon ground states in topological phases of quantum materials.

What makes this work is:

(1.) our recent result that wavefunctions of realistic and technologically viable anyon species – namely of $\mathfrak{su}(2)$-anyons such as the popular Majorana/Ising anyons but also of computationally universal Fibonacci anyons – are reflected in the twisted equivariant differential (TED) K-cohomology of configuration spaces of codimension=2 nodal defects in the host material’s crystallographic orbifold;

(2.) combined with our earlier observation that such TED generalized cohomology theories on orbifolds interpret intuitionistically-dependent linear data types in cohesive homotopy type theory (HoTT), supporting a powerful modern form of modal quantum logic.

Not only should this emulation of anyonic topological hardware functionality via TED-K implemented in cohesive HoTT make advanced formal software verification tools available for hardware-aware topological quantum programming, but the constructive nature of type-checking a TED-K quantum program in cohesive HoTT on a classical computer using existing software (such as Agda-flat), has the potential to amount at once to classically simulating the intended quantum computation at the deep level of physical topological q-bits.

This would make `TED-K in cohesive HoTT an ideal software laboratory for topological quantum computation on technologically viable types of topological q-bits, complete with ready compilation to topological quantum circuits as soon as the hardware becomes available.

In this short note we give an exposition of the basic ideas, a quick review of the underlying results and a brief indication of the basic language constructs for anyon braiding via TED-K in cohesive HoTT. The language system is under development at the Center for Quantum and Topological Systems at the Research Institute of NYU Abu Dhabi. Further details are available at: https://ncatlab.org/schreiber/show/TQCinTEDK#FurtherDetails