A TYPE SYSTEM IS A SEARCH ORACLE

Summary from the TLDR newsletter

Models tend to output better Rust than C++, and better Lean than either. Programs in Rust compile after being checked for a specific and useful set of properties that the checker cannot be talked out of without writing a lexically visible, greppable admission. C++ compiles carry far less information than in Rust, which means more code will compile even if there are errors. Lean allows for brute force due to its cheap verifier, which is why models are unreasonably good given how little code they have been trained on.