Hacker News new | ask | show | jobs
by MaxBarraclough 2055 days ago
> You can prove in math your design will work

It's possible, but extremely labour-intensive, to mathematically prove the correctness of a program. I mentioned this in my previous comment.

> In Programming, unless you are working at switch levels, how could you prove your code is most optimized?

'Most optimised' is an entirely different problem than 'your design will work'.

Complexity theory lets us do something like this, but at a more abstract level, rather than at the level of real-world performance on a particular machine.

As you say, real-world code is almost guaranteed not to be perfectly optimal in terms of performance. We really never need to aim for this though. Market forces push for high correctness and performance, to varying degrees across different different problem domains. Performance matters in game-engines and for high-frequency trading, and in those applications, the software engineers put in great effort to optimise their systems, using fewer abstractions.

Sometimes the software engineering challenge may be a life-critical hard-real-time system, such as in medicine or aviation. Software engineers are able to deliver such systems. It's not of great concern that these systems aren't perfectly optimal in terms of their performance, provided the programs give the right outputs and always meet their deadlines.

The generation of perfectly optimised code has been researched, branded superoptimisation, [0] but it's little more than an academic curiosity. I doubt it will ever be possible to scale it up to be practical for large programs. (I'm not sure if/how they deal with the way most modern processors are terribly complex and don't have easily predictable performance.)

> Abstraction has removed the possibility of doing that.

It's very often a sound decision to trade off on performance in order to gain on some other dimension, such as development velocity, or maintainability, or indeed correctness, given the project's resource constraints. As tools improve, the Pareto frontier advances, and we get a little closer to being able to 'have it all'.

An example of this might be the use of Rust for web development work, which can apparently greatly improve performance (or greatly reduce the computational resources needed). It can bring the performance of C++, while retaining many of the advantages of safer, higher-level languages like Java and C#.

Whether it does this well enough to really grain traction, we'll have to wait and see, but I think it's a good example.

> The closest thing I've seen to Engineering in the Programming world is Industrial Engineering.

Industrial engineering is an entirely different discipline than software engineering.

For examples of 'proper software engineering', the obvious candidates are avionics (as discussed in the article I linked above), and development methodologies involving formal methods, such as with the Tokeneer project. [1][2]

[0] https://en.wikipedia.org/wiki/Superoptimization

[1] https://blog.adacore.com/tokeneer-fully-verifed-with-spark-2...

[2] [Huge PDF] http://www.adacore.com/uploads/downloads/Tokeneer_Report.pdf

1 comments

We may be talking past each other as your points aren't relevant to Engineering.

I'm going to highlight this-

Engineering is Science and math vs Programming which is optimization.

Software engineering is an optimisation problem in the same sense that other engineering fields are optimisation problems. There are tradeoffs to be made on many dimensions, just like in any engineering discipline.

Again, mathematical tools can be used to prove the correctness of programs.

I think you are missing the science and math aspect of this. This isn't a contest. Physicians make lots of money by following tradition and practicing medicine as an art. There is huge debate that Physicians could lose their monopoly powers if medical is a science.
This is vague. Please clarify your point. What aspect are you talking about?