3 ms·

Software engineering is so weird -- what you've just described sounds awful to me. I believe almost the exact opposite of everything you've said. Yet I have no

• bob1029 5y ago
  Willingness to tolerate formal methods does not mean you always have to endure pain and suffering. On the contrary, you may find that you are shipping software that is so good you begin to see the value. For a lot of shops, the problem domain probably isn't complex enough to justify intense formality in the process (i.e. engineering). Once you are dealing with monsters like supply chain or factory automation, you can't play games anymore.
  • Epa095 5y ago
    > On the contrary, you may find that you are shipping software that is so good you begin to see the value. You may also find that when you finally do ship, everyone had started using your competitor, or that your customers needed something slightly different, or that the cost of waiting for you was so high it would have been better having something early. I have great respect for formal verified software, I have even touched on it a bit during my PhD, and there are definitely places for where it makes sense. Same for formal methods in general. But there are other software tasks where it is not just 'not needed' but it is actually the wrong choice. It depends a lot on the opportunity cost of delivering later, and on how well defined the tasks are, and how preffesional the customer is. And the tasks where less formal methods are the right way are not "playing games", they are solving the problem under a different set of constrains, also doing software engineering.
  • feoren 5y ago
    I wasn't recoiling at the fact that you use formal methods, actually. I know it's too late for this comment to be seen, but let me actually point out where my "opposites" are by marking up your comments with my version in [brackets]. Admittedly I'm filling in gaps with my own assumptions about what you mean, and you might agree with me more than I think. > Software engineering can only exist with an incredible amount of discipline. [exploration, creativity, iteration, and discussion are more important than discipline, otherwise you'll be very disciplined in building the wrong thing. This applies at every point of the software lifecycle, not just the beginning!] > We routinely start new implementations in excel [start as you mean to continue. If you prefer Excel over your programming toolset, you should focus on improving your programming toolset. Excel might help with quick mockups and proofs-of-concept, but should not be the basis of your formal design. Your code should!] and perform formal normalization checks over models before writing any code [you should strive to make your code itself the formal document. Code isn't the output of the design, it's the actual design document itself. Instead of separately "proving" things about your code, write your code as you would write the proof]. > You can get away without having a strong type system [why are you trying to take the "formal" part out of your code and into some other document? Apply your rigor and discipline to the code itself, not some other design document! Strong type systems help you do this.] as long as your tables and relations are clean. [the database is "just" a persistence layer and you're locking yourself into a brittle design if its schema permeates the rest of your codebase. This is probably why you include so much upfront design in your process: you're making way too many early decisions at the database level.] This stuff is so powerful. > Figuring out how to funnel your domain instances into a SQL db [everyone seems to assume you need to build your application entirely around a relational database. Build your application around what you want to be able to do, and keep your DB as a storage layer!] and writing all your complex logic in terms of basic queries [write your complex logic in code as close as you can to how you would write a requirements document. Simple queries are great but they're the output of a good middle-tier, not a primary representation.] is how you can build an ecosystem in which determinism [huh? "Determinism" is an unexpected word there. You shouldn't struggle with determinism if you use immutability everywhere you can, except maybe in advanced UI use cases] and formal proofs of correctness are possible [again: you should strive to write your code as close to a "formal proof" as you possibly can, instead of treating the proof as a separate step]. > For me, software engineering is about correctness for the business end. There is certainly still a layer of craftsmanship below the engineering realm which enables all the magic. This is where things like performance and reliability live. Interacting with the outside world is an icky thing, and the specific implementation always depends on the use case. [all agreed here] Look: iterative/Agile methods might appeal to "cowboy coders" who eschew discipline and formal methods, and that gives them a reputation for being associated with "move fast and break things". But they are not inherently less formal than traditional/waterfall "big up front design" methods. The big difference is not a question of "how disciplined should you be?", but rather "where does the discipline go?" Traditional/waterfall methods say "the discipline goes at the start of the project, in big design documents that are separate from the code. Then, later, you code". Iterative/Agile methods say "no, the discipline is maintained throughout the entire project lifecycle and is integrated into how we plan and write the code and manage the ongoing evolution of the project."