Portrait of Michal Moskal

Michal Moskal

Principal Research Software Development Engineer

About

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 and Tom Ball, 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.

Shorter version:

Michał Moskal works at Microsoft Research in Redmond on programming languages and related topics. In the past Michał has worked on software verification and automated theorem proving. Between 2007-2010 he was instrumental to development of VCC—a formal verifier for concurrent C programs utilizing SMT technology, which still 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 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 and Tom Ball, 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.

Yet shorter version:

Michał Moskal works at Microsoft Research in Redmond on programming languages and related topics. In the past Michał has worked on software verification (including VCC – a state of the art formal verifier for C programs) and automated theorem proving. In the past decade Michał has worked on programming experiences for beginners. In 2010, with Nikolai Tilmann, he started Touch Develop for programming phone on a phone, later adopted a programming environment for the very popular BBC micro:bit. In 2016, with Peli de Halleux and Tom Ball, Michał started Programming Experience Toolkit (PXT), which has grown into Microsoft MakeCode – a platform for creating domain-specific programming experiences for beginners, especially in education.

Projects

Publications

Videos

Downloads

English
Français du Canada English