Portrait of Michal Moskal

Michal Moskal

Principal Research Software Development Engineer


Michał Moskal works at Microsoft Research in Redmond on software verification, automated theorem proving, and programming languages. During his PhD studies at the University of Wrocław in Poland he has developed Nemerle—a high level programming language for the .NET platform, and (using Nemerle) Fx7—a satisfiability modulo theories (SMT) solver.

While finishing the PhD he joined European Microsoft Innovation Center in Aachen, Germany in early 2008 and was instrumental to development of VCC—a formal verifier for concurrent C programs utilizing SMT technology. VCC represents the state of the art in semi-automatic C verification and has been used on tens of thousands of lines of industrial C code.

In late 2009, after receiving the PhD degree with honors and prime minister award, Michał has moved to the RiSE group at Microsoft Research Redmond and continued to work on VCC while also taking on other projects including Boogie intermediate verification language, SPUR tracing JIT, and DKAL authorization engine. In late 2010, Nikolai Tillmann and Michał have started Touch Develop—an effort to create an integrated development environment for writing programs on the phone for the phone. Starting in late 2014 Touch Develop was adapted as a programming environment for the BBC micro:bit, as it was rolled out to 700,000 kids in the UK.

In early 2016, Michal, quickly joined by Peli de Halleux, started Programming Experience Toolkit (PXT), which during the following year has grown into Microsoft MakeCode. MakeCode is a platform for creating domain-specific programming experiences for beginners, especially in education. The domains are microcontroller boards (including micro:bit), specific games (eg., Minecraft), a simple game console, augmented reality toolkit, etc. Programs are written using graphical language based on Google Blockly or in a subset of TypeScript, being able to freely switch between the two. TypeScript is also used for specifying and extending the specific experiences, in an open-ended way.