Hacker Newsnew | past | comments | ask | show | jobs | submitlogin

In some sense software engineering is more rigorous than mathematics, because proofs are generally informal, apart from those written in Lean, while all computer programs are strictly formal, as otherwise they wouldn't be machine-readable.
 help



I see what you are sayings. That's an interesting point of view.

Perhaps we should define what rigor means.

Your point is that code is executable and speaks for itself whereas a Math proof (non-lean) is just someone's writing on a piece of paper.

Now let's compare the "practice" of doing Math and software engineering. In Math, every step is very intentional, and getting to a point where a proof is complete and correct is a very long, laborious, difficult and intentional process. Not to mention, the work is also peer reviewed (for published stuff). This is what I mean by rigor.

In software engineering, the practice is quite different. We defined the problem (somewhat), come up with a design that we "think" would work, write programs that we think is correct and then execute it. Most of the time it doesn't work exactly as we would have predicted. So we take the signal and adjust. So it's a more iterative part and this gets us closer to reality (what we actually want it to be), step by step.

So comparing the two, the major difference I see is in one each and every step is very intentional and we can't guess it. While in the other one we have lots of liberties, but we are still making progress.

So to me the difference is just between the practices followed in the field when it comes to rigor.


Maybe a similar comparison would be this: for proofs, the standards of correctness are purely internal and can in principle be formally defined, as in Lean. The formal conjecture has to follow from the premises. Either it is proven or not. In contrast, in 99% of ordinary software, no fully formal standard of correctness exists. The requirements are informal. So what counts as a bug and what doesn't is a judgement call that can only be checked by asking the person who wanted the software whether it works as intended.



Guidelines | FAQ | Lists | API | Security | Legal | Apply to YC | Contact

Search: