Re-think your assumptions about "mathematical proofs". Compiling software with types is a mathematical proof. We get certain guarantees "for free" without even

Re-think your assumptions about "mathematical proofs". Compiling software with types is a mathematical proof. We get certain guarantees "for free" without even thinking about it. It's immensely useful and flexible. We can build better type systems than are in common use. So much more is possible than just making sure we don't stick an int where a string is supposed to go. Moving forward is about raising the bar on what we get "for free". We have a lot of experience building programs that help us program (e.g. compilers, IDEs, build systems) We can move forward without falling into traps (low performance, high programmer knowledge required, overly rigid, more work required than gained in productivity) There are no silver bullets but we can continue to improve.