C++ comes with baggage and requires up-front training. You need to dive into every language feature and STL library, learn how compilers implement stuff, then decide what to use and what not to, and the decision often depends on context. It has a high cognitive load in my opinion for that reason. But once you do that, you get a relatively high-level language that can go as low and be as fast as C.
I'd say it's being able to structure your data however suits your problem and your hardware, then being able to look at a profile and being able to map read/writes back to source. Both C and C++ excel at this.
The advantage of C++ over C is that, with care, you can write zero-cost abstractions over whatever mess your data ends up as, and make the API still look intuitive. C isn't as good here.
According to my experience, all the "zero-cost abstractions" from C++ most of the time make it more annoying to maintain and/or understand the code, especially with respect to resource management, introduce compatibility issues at the toolchain level, and - even when looking perfect in toy benchmarks - are often not even zero-cost (e.g. all the bloat the templates generate often hurts).
Clickbait title, the proved part of the program had no bugs?
As an aside, why can't people just write factually? This isn't a news site gamed for ad revenue. It's also less effort. I felt this post was mostly an insulting waste of time. I come to HN to read interesting stuff.
Is it fair when it comes to formally-verified software to only consider bugs that violate a proof, and ignore everything else?
Formally-verified software is usually advertised "look ma no bugs!" Not "look ma no bugs*" *As long as this complicated chain of lemmas appropriately represents the correctness of everything we care about.
In boating theres often debate of right of way rules in certain situations, and some people are quick to point out that giant tanker ships should be giving way to tiny sailboats and get all worked up about it*. The best answer I've heard: they're dead right! that is to say as right as they are dead (if they didnt yield) lol. In the same vein, I think someone who assumed that a formally-verified software was perfect and got hacked or whatever is going to be a bit wiggly about the whole thing.
* = Technically the rules prioritize the tankers if they are "restricted in ability to maneuver" but everyone loves to argue about that.
Nobody with experience in the field advertises formally-verified software like that, and it is understood that the spec may as well be wrong. It is also understood that the non-verified parts may have bugs (surprise). There is no news here.
Unless "with experience in the field" == academia, disagree. In particular I remember the early discourse & hype around Wireguard, it was discussed as if perfection was an achieved outcome.
Yeah, extremely misleading title even if it is technically true semantically. The phrasing gives the impression that a bug was found in `lean-zip` as part of the proof boundary when it was part of the unverified archive-handling code.
The archive-handling code was in lean-zip, it just seems the verifiers forgot to write proofs for it (still a bug).
Thats not the main finding of the article however. The main bug found was actually in the lean runtime, affecting all proofs using scalar arrays where the size of the array is not bounded.
Also, he even just created the second bug out of thin air. There is no code reference, and the reason why he downplays it is because he knows that if someone looks into it, they will realize he misrepresented the actual code.
I also like how, according to Github, the repo is 99.7% HTML and 0.3% C++. A testament to the interpreter's size, I guess?
reply