In this meeting we would like to discuss the development of the Mist programming language. Our goal is to create a new programming language with many promising features, prominently among them an integrated proof framework. The hope is to automatically generate formal proof of correctness, rather than relying solely on run-time checks. This framework may also offer new opportunities for code optimization. Rather than optimizing common cases of existing programs, we propose to make more elegant code less costly to run, and we design Mist accordingly.