FwPython, Part 1: Setting the Stage

FwPython is a compact, Python-like object-oriented language formalized in Lean 4, built to put controlled pressure on the parts of Python typing that type checkers actually have to reason about. This first post sets up the source language and runtime model.