> 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.

The real fiscal burdens on your society are your military spending and the interest on the debt you have already taken on.

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.

But still, Lean is executable and can be used as an ordinary programming language.

I'm wondering why my submission, made 22 hours ago, is marked as a duplicate, but this submission, made just 12 hours ago, isn't.

https://news.ycombinator.com/item?id=47438490

I'm also wondering why the same URL for both submissions isn't recognized as the same, and why the new submission was allowed.

Isn't Yandex a European Google? :D

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.

It's important even without the meme. c++ has try-catch but not try-finally.

It is common for some titles to exceed the allowed length limit on HN. I often do not have enough time to contemplate the best way to shorten them.

The source repository is here: https://github.com/CorsixTH/CorsixTH

Rainier had one of the most excellent C++ blogs. He is also the author of several books on modern C++ standards. Rest in peace, Rainer. :(

The author is Jencel P.? I saved this book sometime ago under the author name Boris Marinov? Is this the same person now writing under a different pen name?

Is the same. He seems to obscure himself déliberately.