I wonder how that is compatible with the industry requirements, and even with software engineering in general. A lot of the code we write is short lived, either

I wonder how that is compatible with the industry requirements, and even with software engineering in general. A lot of the code we write is short lived, either because we're iterating, or because features aren't used anymore. Also, bugs aren't the end of the world most of the time. You don't aim for 100% correctness, but for something that provides value to users and it's better than your competitors. Formal proofs may be useful in some case, but I don't see them outside very niche fields. Even regular static types can be argued against.