Warning: Some posts on this platform may contain adult material intended for mature audiences only. Viewer discretion is advised. By clicking ‘Continue’, you confirm that you are 18 years or older and consent to viewing explicit content.
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.
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.
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.