Hacker News new | ask | show | jobs
by pjc50 4114 days ago
Compound knowledge works in maths, because of the solidity of proofs. You don't wake up one day and find that you need to update all your existing proofs to Axiom Of Choice 11.3.5 in order to fix a critical security bug.

Programming has weak versions of this: if all your libraries typecheck, then you can write a typecheckable program with them.

Functional languages get a lot closer to reliable composition, but things that modify state are a lot harder to reason about because the state space just explodes. And you can of course write in Coq or do formal verification in Z - it's just much more time-consuming. As an industry we'd rather get to market first than get the product 100% reliable.

1 comments

> Compound knowledge works in maths, because of the solidity of proofs

Yes, I didn't mean to compare them 1 to 1 but more of in concept.

> As an industry we'd rather get to market first than get the product 100% reliable.

Very true and as long as security isn't core focus of your app I think this is just fine.