If we accept this definition, C++ already seems to be many different languages. At my job, I'm currently fighting floating-point determinism issues across different build configurations, compilers, CPUs, operating systems, and standard library and libm implementations so that snapshot tests pass with the same hashes on all platforms. I can confirm that this is a complete nightmare.
Yup. I tried hard to not allow D's behaviors to be changed based on a compiler switch. Yes, we have switches to enable certain features, but not silent behavior changes.
It's not perfect, but the forest of such switches in C compilers motivated D to not have them.
Alternatively every flag that changes the semantics of the code is a workaround for either legacy code no one will fix or language committee decisions that have unintended side effects.
> A hidden metric here is the number of new bugs created by these fixes.
If the project has proper test coverage, there should be no significant number of new bugs. This is no different than the possible regressions added by a human-implemented feature.
And LLMs have made implementing a massive number of tests far easier and faster than before the LLM era.
Interest and military and take a distant third and fourth place respectively. Here are the rough proportions of the top US federal budget expenditures according to the Treasury Department:
- Healthcare (Medicare and Medicaid): 24%
- Social Security: 23%
- Net Interest on Federal Debt: 15%
- National Defense: 13%
And I'll point out that the enormous bill for the interest on debt is a pretty good reason to avoid ringing up so much debt in the first place.
What about the performance characteristics of the Lean programs? I know it is a natively compiled language, but is the code it produces comparable to that of modern system programming languages in terms of performance?
Oddly enough, most uses of Lean never actually run the program. The fact that it type checks is enough to prove the theorem in question.
That said, if execution is seriously required for your problem along with strong logic on the side, you may prefer Dafny which transpiles the computation part of your proof to C++ or Go.
More interesting to me is the actual algorithm that the software uses and whether it is practical to apply it with pen and paper in an actual competition, if the number of steps is not too high, of course. Unfortunately, the article didn't go into that depth.
I intentionally shortened the title because there is a length limit. Perhaps I didn't do it the right way because I was unfamiliar with the mentioned meme. Sorry about that.
I think that a compiler option should control this. It can be a nice optimization, but the programmer should be able to opt out.
reply