Capital-A abstraction means lambda calculus. Compiler too dumb means you can't just program with functions & write said Abstractions (which map cleanly to proofs via HC) in Rust because it does not handle them well.

There we go :)