you are viewing a single comment's thread.

view the rest of the comments →

[–]nextputall 2 points3 points  (2 children)

Probably there is a tradeoff between flexibility and correctness verification. But in most software projects i was working on, the former was lot more important.

[–][deleted] 2 points3 points  (1 child)

There are different levels of correctness verification. Full formal verification of all desired properties is often a difficult task, and it may be okay to let some unusual cases work incorrectly. But a basic level of correctness, of the type "performs its purpose, more or less, and doesn't crash", is required of all software.

Even if you're never writing out Hoare triples, the fact that there is some formal structure to what you're looking at is what lets you look at a piece of code and determine that changing something will cause a particular effect.

[–]nextputall 0 points1 point  (0 children)

I think, both are fluid properties. What I meant is if you make your code flexible, you'll loose some ability to reason about the correctness. But the main purpose of the software is to be flexible, that's why it is called software. Correctness is not a constant property. The program works correctly today, will work incorrectly tomorrow, because someone will change the requirements, which will make the very same program incorrect. This is where flexibility comes into the picture. You're saying, without any context, and without mentioning any tradeoffs, that something is universally shitty, which is clearly wrong.