[stereolambda]

The part how the whole system can be proved correct, but still break and bug out as handled and understood by its users and maintainers, to me summarizes practical problems with the formal trends in software engineering. Abstractions break all the time, starting with the type systems. Once you introduce something like this, you have to feed the system that you built, and then as a second consideration do what you actually want/have to do.

I can see the intellectual appeal and even the argument for formalism in some high-risk areas. I guess I am most burnt by the advent of hyperlinted, theatrically "typechecked" enterprise Python. I don't think people pushing this stuff would have the balls to introduce an actually formal environment, since even Java is there, not to mention ML-style languages, Rust etc. Maybe there's fear about the staffing and scary appearance, which the article also mentions. (I still sincerely wait for a bigger niche for functional and lispy shops, maybe when the industry transforms with de-monopolization.)

But there is a common thread in the bad kind of arguing for formalisms, where the Scotsmen are never true and your lazy human mind isn't Godlike enough to reason about the program correctly from the start. I actually like how TFA moves toward communicating better so maybe conversations could be more productive in these aspects.