(a) "Proof of security" is a term of art that doesn't mean what it sounds like. In cryptography, you "prove" specific things about an algorithm, often in the context of a "game" with one or more adversaries. You need to know more than that an algorithm has a proof; you also need to know which proofs those are, and how they apply to your application.
(b) Proofs generally apply to algorithms and low-level constructions. Once you start composing proven primitives into whole cryptosystems, typically, all bets are off. Proofs of entire protocols are an active research area.
(c) A proof will almost always apply to the abstract, mathematical notion of an algorithm or construction, not to the code that might implement it.
I apologize in advance at how little this has to do with the actual resource linked here; I'm just sort of predicting what the thread on HN, if any, would look like.
Good points. Far as code proofs, I think you should look at Microsoft's VerveOS (safety not security), seL4 (security), Astree, and the SPARK-based security projects. They all prove aspects of the code itself. The old A1 projects also typically mapped a low-level spec to code with many things at or near a 1-to-1 mapping. Very low risk of a misrepresentation or abstraction gap attack when done that way.
I still always encourage them to combine their efforts with thorough testing, code inspections, static analysis, and careful source-to-object code validation. Most of that is even required in the high assurance standards. Takes a lot more than proofs, code reviews, or tests in isolation to begin to make a strong security argument. As you know, it's so labor intensive and requires such specialist skills that almost all commercial and FOSS projects skip steps to get running code out the door. That's why penetrate and patch will always be the norm with highly secure systems always several versions worth of features behind mainstream. If they have them at all...
Regarding (c), if your program is written say Agda[1], the code can come with a proof that it has the mathematical properties you want. Or rather, your implementation might simply be the proof.
I'd guess that (c) refers to the fact that implementation details can expose the algorithm too, e.g. side-channel attacks, leaking timing info, and so on... Things like constant-time comparisons are not generally part of the consideration of the algorithms and proofs (imho).
(a) "Proof of security" is a term of art that doesn't mean what it sounds like. In cryptography, you "prove" specific things about an algorithm, often in the context of a "game" with one or more adversaries. You need to know more than that an algorithm has a proof; you also need to know which proofs those are, and how they apply to your application.
(b) Proofs generally apply to algorithms and low-level constructions. Once you start composing proven primitives into whole cryptosystems, typically, all bets are off. Proofs of entire protocols are an active research area.
(c) A proof will almost always apply to the abstract, mathematical notion of an algorithm or construction, not to the code that might implement it.
I apologize in advance at how little this has to do with the actual resource linked here; I'm just sort of predicting what the thread on HN, if any, would look like.