Low-cost microcontroller boards like the BBC micro:bit are used to engage and inspire students worldwide to learn more about computing. Easy-to-use web-based programming environments and low-cost hardware allow novices to build physical computing systems with the micro:bit – systems that sense and respond to the real world. However, devices such as the micro:bit may not capture the attention of every student, as the interests of some may lie in graphic design, animation, or other areas that are not the main focus of physical computing.

We present TileCode, a video game creation environment that runs on battery-powered microcontroller-based gaming handhelds. Our work is motivated by the popularity of retro video games, the availability of low-cost gaming handhelds loaded with many such games, and the concomitant lack of a means to create games on the same handhelds. With TileCode, we seek to close the gap between the consumers and creators of video games and to motivate more individuals to participate in the design and creation of their own games. The TileCode programming model is based on tile maps and provides a visual means for specifying the context around a sprite, how a sprite should move based on that context, and what should happen upon sprite collisions. We demonstrate that a variety of popular video games can be programmed with TileCode using 10-15 visual rules and compare/contrast with block-based versions of the same games implemented using MakeCode Arcade.

Transformations over assembly code are common in many compilers. These transformations are also some of the most bug-dense compiler components. Such bugs could be elim- inated by formally verifying the compiler, but state-of-the- art formally verified compilers like CompCert do not sup- port assembly-level program transformations. This paper presents Peek, a framework for expressing, verifying, and running meaning-preserving assembly-level program trans- formations in CompCert. Peek contributes four new com- ponents: a lower level semantics for CompCert x86 syntax, a liveness analysis, a library for expressing and verifying peephole optimizations, and a verified peephole optimiza- tion pass built into CompCert. Each of these is accompanied by a correctness proof in Coq against realistic assumptions about the calling convention and the system memory alloca- tor. Verifying peephole optimizations in Peek requires prov- ing only a set of local properties, which we have proved are sufficient to ensure global transformation correctness. We have proven these local properties for 28 peephole transfor- mations from the literature. We discuss the development of our new assembly semantics, liveness analysis, representa- tion of program transformations, and execution engine; de- scribe the verification challenges of each component; and detail techniques we applied to mitigate the proof burden.