3 ms·

On the other hand, in many cases what's defined as the "bare minimum" ends up being more than expected. The corner-cutting approach ends up pricier than the tho

On the other hand, in many cases what's defined as the "bare minimum" ends up being more than expected. The corner-cutting approach ends up pricier than the thorough approach in the long run, because it must be constantly adjusted if not entirely re-done. e.g. building a bridge to support a city's normal traffic density, but the city ends up growing, and the way the bridge was designed makes adding reinforcement difficult. Or building a bridge whose materials start to melt at a certain temperature that's above what's expected for the region, but climate change raises the temperature over the threshold, so it needs a completely different material. Hence the article's point that software companies should invest in formal methods, because while formally proving something is a long process without much reward in the short term, it eliminates an entire class of bugs which, in some long-term projects, makes it worth the effort.

vlovich123 2y ago
Conversely, we also know that taking longer to build something scalable is more expensive than just building cheaper things that accomplish the job now and solving the bigger problems when they’re relevant to the point where it can be the tipping point of success in the first place. In other words, that super reliable bridge that can handle all the growth you throw at it can take longer and too much money and result in a city that fails to have a growth problem in the first place. We know that’s true experientially in both CS (YAGNI) and in the physical spaces (eg Wright brothers constantly iterating with cheap prototypes until they figured out something that worked and SpaceX doing similar things with their prototypes). Iteration = learning. In theory formal methods let you iterate at a cheaper phase of the project. In practice, the methods themselves are very difficult to scale to large projects and these days require you to build the project twice - once for the formal language and then hand-translated to a production language.

vlovich123 2y ago

Conversely, we also know that taking longer to build something scalable is more expensive than just building cheaper things that accomplish the job now and solving the bigger problems when they’re relevant to the point where it can be the tipping point of success in the first place. In other words, that super reliable bridge that can handle all the growth you throw at it can take longer and too much money and result in a city that fails to have a growth problem in the first place. We know that’s true experientially in both CS (YAGNI) and in the physical spaces (eg Wright brothers constantly iterating with cheap prototypes until they figured out something that worked and SpaceX doing similar things with their prototypes). Iteration = learning. In theory formal methods let you iterate at a cheaper phase of the project. In practice, the methods themselves are very difficult to scale to large projects and these days require you to build the project twice - once for the formal language and then hand-translated to a production language.