# Quantum Calculi--From Theory to Language Design
## 5 Conclusions  
Quantum programming theory is a dynamic and vital research field. In the last twenty years, several languages have been introduced and implemented. Quantum lambda calculi provided the basis for quantum computability, establishing the equivalence with other computational models. Foundational languages helped in developing ad hoc type theories for the sound management of data according to quantum mechanics principles. More practical languages showed how to program simulated and real small devices, in the perspective of the availability of a universal, powerful quantum device.  
Different design choices bring different benefits and weaknesses. The choice of the QRAM architectural model, which assumes a strong separation between data and control, allows to efficiently manage the restrictions due to programming with quantum data. Moreover, it seems to be the more realistic architecture for physical implementation. Concerning the design of the type system, in this paper, we met several solutions. Linear Logic (LL) perhaps remains the most natural option for quantum type systems, since LL modalities allow to syntactically distinguish between duplicable and non-duplicable resources and reduction strategies can easily preserve the no-cloning properties of quantum data. Nevertheless, different solutions such as the use of dependent types are emerging as valid alternatives. This holds both for \"stand-alone\" languages (such as qPCF) and for embedded languages, in which the quantum core is purely linear and neatly separated from the \"host\" part, as happens in QWIRE and Quipper. This classification can be central to the scope of a language. On the one hand, a stand-alone calculus can represent a better solution if one is interested in theoretical studies since good properties (of the type system or the operational semantics) do not depend on the properties of the host language. On the other hand, an embedded language allows more direct control of quantum operations and is suitable for the implementation in automatic verification systems.  
Concerning the denotational semantics of quantum languages, an argument we did not address in this paper, many fascinating theoretical results have been shown extending to the quantum setting different techniques and tools (as the Geometry of the Interaction or several categorical frameworks) and various challenging questions remain open [44; 45; 52; 60].  
We conclude that the theoretical results of the last decades and the current technological development seem to happily converge in the same direction. The advances of quantum technologists, that year-by-year provide more efficient architectures, also suggest how quantum computers have to be programmed. For example, the NISQ (Noisy Intermediate-Scale Quantum) technology, available shortly, is providing important steps toward bigger and fault-tolerant computers and could early become a concrete reference for realistic software design [61]. Thanks to this parallel effort, today we can design increasingly efficient languages and run quantum algorithms on both simulators and real prototypes [1]. At the same time, formal verification of quantum programs (e.g., based on logic [62; 63] or on mechanizable tools [64]) became an urgent and exciting challenge. We are entering the quantum future and we are ready to program it.  
This research received no external funding.  
Acknowledgments:I wish to dedicate this paper, that embraces one of the passions of my life, to four very special people that, day-by-day, make me happy: my beloved-hippie-super-mom [PERSON] (the genius of the family), my brother-friend-uncle [PERSON] (the cub of the family), my friend-confident-maitre [PERSON] (the [PERSON] of our Department of Computer Science) and my best friend [PERSON] (who, in the last 20 years, has shared with me secrets, drinks and football-related joys and sorrows). Thanks, dears, for all. Long and prosper life.  
**Conflicts of Interest:** The author declares no conflict of interest.