I’m honored to have been chosen by Microsoft as a Most Valuable Professional for F#, and the recent 5 days I spent at the annual MVP Summit were thrilling, stimulating, and eye-opening. While I can’t talk about much of what I learned and participated in, I want to pass on some great things that are completely out in the open, yet little known. They are on the cutting edge of philosophical accomplishment, both changing the world, really. And Microsoft Research is implementing these two great ideas with my favourite programming language.

Quantum Computing

The idea of a quantum computer gestated throughout the 1980’s, most famously in a 1981 proposal by Richard Feynman. The early 1990’s saw the discovery of the first quantum computing algorithm (one that could provably do something much faster than any classical algorithm) and by the middle of the decade Shor’s Algorithm became the first quantum algorithm that could do something really interesting (and spawned a whole genre of misinterpretation of quantum computing capabilities in popular journalism).

MSR is at the forefront of quantum computing research with LIQUi|> (pronounced “liquid”), the most advanced platform for quantum computing simulation in the world. There are no universal quantum computers in the world, yet. Until there are, LIQUi|> plays an important role in evaluating quantum computing capabilities, for instance in physical processes (the real intention of Feynman’s original work), and in providing a platform to evaluate academic work in the field. And it is poised to be the world’s first quantum computing development environment as soon as enough qubits can be entangled to build the worlds first quantum computer.

You can learn more about LIQUi|> in this video and accompanying slides.

The Computational Science Trinity

Here’s another idea, the Trinity of Computational Science. Frequently expounded upon by Robert Harper of Carnegie Mellon’s CS department, this is the unity of Type Theory, Proof Theory, and Category Theory. Taking it down a level towards the practical, think of it as Type Systems (strong typing), proving program correctness, and Functional Programming. The Oregon Programming Languages Summer School (sponsored in part by MSR) is dedicated to teaching these foundations to advance research and practical software engineering.

This is another area of leadership by MSR. This time with a derivative language of F# called F* (F Star). This language and others, like Idris, implement dependent types, an extension of type theory beyond the familiar strong typing of F#, where types can depend on functions, but F* takes it to another level. By interfacing to MSR’s Z3 theorem prover, F* effectively unifies the Computational Science Trinity. Functions and types become manifestations of the same thing and directly connect to correctness proof.

You can download F* and/or work through the interactive tutorial and experiment with it online.