5 ms·

I don't think you can teach software engineering. Writing software is more like writing proofs than building airplanes. Take a formally verifiable language like

by ipnon 7y ago

I don't think you can teach software engineering. Writing software is more like writing proofs than building airplanes. Take a formally verifiable language like Agda for example. Proofs are indistinguishable from programs in that language. The Curry-Howard correspondence shows this is true for program-proofs in general. Large software systems fail continuously in countless ways all the time. Google search will still throw 404 or 5xx occasionally. We're not building airplanes that either fly or crash (although even the software running airplanes is now increasingly fault tolerant). We are effectively getting from point A to B through a variety of logical operators, increasing the set of valid A through trial and error. We find an input that throws error, our theorem was faulty and we update our proof. A seemingly valid input can't produce the results we want, we double check to make sure our proof is still valid. Dilettante engineers will begin to introduce unbound complexity at this point for making fixes without understanding root causes. For the above reasons, we should abandon any attempt at comprehensive software engineering curriculum or canons. We are not architecting a skyscraper to be delegated to a construction company to be built one and done for all of time. We are continually exploring and staking out a specific problem space. Our greatest compass in these new journeys will always be foundational computer science. We must take the specific and make it general. Careful application of elementary data structures, algorithms and discrete analysis will move and has moved us continents further than any convention to "best practices" ever will.

kaymanb 7y ago
Funny, I'd say that writing proofs is a lot like building an airplane, and software engineering might be far away from both. In writing a proof, you provide an argument that justifies some claim is true. Your argument has to be airtight, so that no matter what kind of counter example or ugly scenario is proposed, your argument still holds. The same seems true for an airplane. It needs to do its job (fly) and do so on the face of a myriad of different external factors. If you build a plane, it should "never" fail. Software on the other hand, can be built without thinking about ALL of these edge cases. Obvious it's better if it always works, but it's usually okay if there is some bizarre scenario that causes an error. For some pieces of software it might even be okay if these errors never get fixed (ie: a very small number of users ever experience them). Software can work, even when it (kinda) doesn't. The Curry-Howard correspondence might be technically true, but we're just as bad at writing specifications for programs as we are at writing the programs themselves. It could be good to acknowledge that and just write the software that solves most, but maybe not all, of our problems.
deleted 7y ago
[deleted]
crimsonalucard 7y ago
Although programs function in an ideal universe amenable to proof and theory and therefore perfect for calculation and theoretical approaches rather than engineering "best practices," what you describe has not been the case in the industry. The irony is airplanes live in a unideal universe where no theory can predict anything to a perfect degree and testing must take precedence. However when building an airplane, aerospace engineers use far more theory than software engineers even when testing and engineering best practices is an absolute requirement for the unpredictable nature of real world physics acting on an airplane. I feel the reason why the world is the way it is is due to necessity. A buggy program is (usually) an annoyance. A buggy airplane is (always) a disaster. It is necessary to prevent disasters but it is not necessary to eliminate an annoyance.

by ipnon 7y ago

kaymanb 7y ago

Funny, I'd say that writing proofs is a lot like building an airplane, and software engineering might be far away from both. In writing a proof, you provide an argument that justifies some claim is true. Your argument has to be airtight, so that no matter what kind of counter example or ugly scenario is proposed, your argument still holds. The same seems true for an airplane. It needs to do its job (fly) and do so on the face of a myriad of different external factors. If you build a plane, it should "never" fail. Software on the other hand, can be built without thinking about ALL of these edge cases. Obvious it's better if it always works, but it's usually okay if there is some bizarre scenario that causes an error. For some pieces of software it might even be okay if these errors never get fixed (ie: a very small number of users ever experience them). Software can work, even when it (kinda) doesn't. The Curry-Howard correspondence might be technically true, but we're just as bad at writing specifications for programs as we are at writing the programs themselves. It could be good to acknowledge that and just write the software that solves most, but maybe not all, of our problems.

deleted 7y ago

[deleted]

crimsonalucard 7y ago

Although programs function in an ideal universe amenable to proof and theory and therefore perfect for calculation and theoretical approaches rather than engineering "best practices," what you describe has not been the case in the industry. The irony is airplanes live in a unideal universe where no theory can predict anything to a perfect degree and testing must take precedence. However when building an airplane, aerospace engineers use far more theory than software engineers even when testing and engineering best practices is an absolute requirement for the unpredictable nature of real world physics acting on an airplane. I feel the reason why the world is the way it is is due to necessity. A buggy program is (usually) an annoyance. A buggy airplane is (always) a disaster. It is necessary to prevent disasters but it is not necessary to eliminate an annoyance.