Programmer Humor

19551 readers

995 users here now

Welcome to Programmer Humor!

This is a place where you can post jokes, memes, humor, etc. related to programming!

For sharing awful code theres also Programming Horror.

Rules

Keep content in english
No advertisements
Posts must be related to programming or programmer topics

founded 1 year ago

MODERATORS

Feyter@programming.dev

anzo@programming.dev

BurningTurtle@programming.dev

pylapp@programming.dev

113

We did this to ourselves (lemmy.world)

submitted 1 year ago by mikidep@lemmy.world to c/programmer_humor@programming.dev

42 comments fedilink hide all child comments

you are viewing a single comment's thread
view the rest of the comments

[–] deegeese@sopuli.xyz 10 points 1 year ago* (last edited 1 year ago) (1 children)

The problem with formal proofs for code is that it assumes the spec/requirements are complete and bug-free.

I find most bugs come from missed or misinterpreted requirements.

[–] tatterdemalion@programming.dev 25 points 1 year ago* (last edited 1 year ago)

I have a feeling you are misunderstanding what is meant by "theorems for free" here. For example, one theorem that is proven by all safe Rust programs is that they don't have data races. That should always be a requirement for functional software. This is a more pragmatic type of automatic theorem proving that doesn't require a direct proof from the code author. The compiler does the proof for you. Otherwise the theorem would not be "free" as stated in OP.