Michal Moskal

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 (opens in new tab) in Poland he has developed Nemerle (opens in new tab)—a high level programming language for the .NET platform, and (using Nemerle) Fx7 (opens in new tab)—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 (opens in new tab)—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 hundreds 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 (opens in new tab) at Microsoft Research (opens in new tab) Redmond and continued to work on VCC while also taking on other projects including Boogie (opens in new tab) intermediate verification language, SPUR tracing JIT, and DKAL (opens in new tab) authorization engine. In late 2010, Nikolai Tillmann and Michał have started Touch Develop (opens in new tab)—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 (opens in new tab) as a programming environment for the BBC micro:bit (opens in new tab), as it was rolled out to 700,000 kids in the UK.

In early 2016, Michal, quickly joined by Peli de Halleux (opens in new tab) and Tom Ball (opens in new tab), started Programming Experience Toolkit (PXT (opens in new tab)), which during the following year has grown into Microsoft MakeCode (opens in new tab). 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 (opens in new tab) or in a subset of TypeScript (opens in new tab), being able to freely switch between the two. TypeScript is also used for specifying and extending the specific experiences, in an open-ended way.

In 2019, Michal, Peli, and Tom together with James Devine (opens in new tab) and Steve Hodges (opens in new tab) started the Jacdac project (opens in new tab) which brings software abstractions to low-cost plug-and-play electronics.

In late 2021, Michal, Peli, and Tom started DeviceScript (opens in new tab), which is an implementation of TypeScript for tiny IoT devices, building on top of hardware abstraction provided by Jacdac.

In late 2023, Michal with Emre Kıcıman (opens in new tab) started AI Controller Interface (AICI) (opens in new tab) which implements abstractions to constrain and control output of a large language model (LLM) via a binary Wasm interface, and language built on top of it.

Shorter version:

Michał Moskal (opens in new tab) works at Microsoft Research in Redmond (opens in new tab) on programming languages and related topics. Previously, he worked on software verification, including VCC (opens in new tab) – a state of the art formal verifier for C programs, and automated theorem proving. Over the past decade, Michał has focused on programming experiences for beginners. In 2010, with Nikolai Tillmann, he launched Touch Develop (opens in new tab), initially a programming environment for mobile phones, later adapted for the BBC micro:bit (opens in new tab). In 2016, along with Peli de Halleux and Tom Ball, Michał initiated the Programming Experience Toolkit (PXT) (opens in new tab), which evolved into Microsoft MakeCode (opens in new tab) – a platform for creating domain-specific programming experiences, especially for education. This led to Jacdac (opens in new tab), developed with James Devine and Steve Hodges, a system for building plug-and-play electronics. Subsequently, in 2021, they introduced DeviceScript (opens in new tab), a TypeScript implementation for tiny IoT devices. In 2023, Michał, together with Emre Kıcıman, started the AI Controller Interface (AICI) (opens in new tab), which introduces abstractions to manage and control the output of large language models (LLM) via a binary Wasm interface, and a language built on top of it.

Yet shorter

Michał Moskal (opens in new tab) works at Microsoft Research in Redmond (opens in new tab). He has focused on formal software verification (opens in new tab), programming languages (compilers (opens in new tab), interpreters (opens in new tab), runtimes), as well as programming for beginners (opens in new tab), and more recently syntactic constraints (opens in new tab) on output of Large Language Models. His PhD is from University of Wrocław (opens in new tab) in Poland.