3 ms·
> "proving" things about code for working programmers I'd argue that this is antinomic. Proving things about code isn't something working programmers do yet. I
by yodsanklai 2y ago
> "proving" things about code for working programmers
I'd argue that this is antinomic. Proving things about code isn't something working programmers do yet. I'd say that Hoare logic is a good starting point as it is sometimes taught in introductory CS classes.
Coq has a steep learning curve, especially if you're not familiar with OCaml or similar languages. Maybe Why3 is more beginner friendly https://www.why3.org https://www.why3.org
Proving vs verifying: could mean the same thing. Proving seems to me as something more interactive in nature, while verifying could be automatized (model checking, SMT-solving of annotated programs).
- teaearlgraycold 2y agoWorking programmers write proofs in a limited sense. Any time you write types you're writing a proof. Maybe it's a stretch to say "const a: int = b;" is a proof, but when you get into higher-order types in TypeScript it's appropriate.
- samatman 2y agoA trivial proof is still a proof. There's nothing trivial about "const a: int = foo();" though. Compilers disprove the claim by contradiction all the time.