Turns out getting working code is a lot cheaper and more useful than formally proven code.
And maintainable code is even cheaper and more useful than that in the long run.
Ah, the long run. I keep trying to explain this concept to management, but without success.
Yes, that’s why we use typing, to get better working code more easily. That’s why I use type annotation and enforced checkers in Python. It makes it so much easier and quicker to create good systems of any significance.
Cheaper? Yes, I guess so, depending on how you measure cost. More useful? Absolutely disagree.
Industry will pick functionality over verification every time.
Industry will choose not to verify that your function does not produce NullPointerException wasting hours of the client’s work, because in order to do that they would have to have actual requirements for software developers, and in order to do that they would have to 1 - have the managers be actually technically literate, and 2 - pay the developers properly That’s it. That’s the theorems. The “formal verification” we’re talking about here are those of the likes of “this value is a damn integer”, or as you could interpret it “your code is not stupidly broken”.
To be clear, I’m not writing this big comment for you, I know you’re trolling or whatever you’re into, I’m writing this to inform other readers. ✌🏻
Industry will leak PII without consequence every week.
The technical debt is strong in this one
You call it tech debt, I call it last quarter’s profits.
And a lot more bug prone. I’m just explaining the OP because people didn’t get it. I’m not saying dynamic languages are bad. I’m saying they have different trade-offs.
The problem with formal proofs for code is that it assumes the spec/requirements are complete and bug-free.
I find most bugs come from missed or misinterpreted requirements.
I have a feeling you are misunderstanding what is meant by “theorems for free” here. For example, one theorem that is proven by all safe Rust programs is that they don’t have data races. That should always be a requirement for functional software. This is a more pragmatic type of automatic theorem proving that doesn’t require a direct proof from the code author. The compiler does the proof for you. Otherwise the theorem would not be “free” as stated in OP.
deleted by creator
