Hacker News Reader

> instead of working on clearly defined projects with scope and specification

Yes, it's much easier once you get to that point. Getting there is the real work. Wrangling clarity into requirements from messy humans isn't amenable to all the nice formal methods, but it's a very critical part of the work.

View on HN

Could it be that formal methods are exactly the solution to "wrangling clarity into requirements from messy humans"? Business people and programmers could work closely together to incrementally build a list of formal requirements with the help of proof assistants. So that both parties can know clearly what are known to be ambiguous and what can be implemented immediately at every stage of discussion. Update the formal list of requirements whenever anyone has a breakthrough. Investigate into possible inconsistency early on with the help of proof assistants. Enforce project-wide constraints for every update to the list of requirements. Cooperate to make more and more informal stuff formal to reduce misunderstanding.

Formal methods can help with exploration and cooperation.

"Business people" and programmers are inherently incompatible, because there is a clash of interests. What you need in dev team is a programmer who balances possible solutions against requirements, and only their decision counts, and guides the other programmers. "Heya, our software is gonna be great if we add this nifty feature I wrote last week" then the deciding has got to say "save that for the next major release, let's get the requirements working bug-free and testable first!"

Reply on news.ycombinator.com