9 ms·

There are tools such as TLA+ that help with modeling at the level higher than executable code. Recent talk for example: Fifteen years of formal methods at AWS

by d0mine 2y ago

There are tools such as TLA+ that help with modeling at the level higher than executable code. Recent talk for example: Fifteen years of formal methods at AWS Marc Brooker, Amazon AWS https://youtu.be/HxP4wi4DhA0 https://youtu.be/HxP4wi4DhA0

jandrewrogers 2y ago
These don't model key properties of software for systems engineering purposes. Software can be technically correct in a formal sense and also broken in all real implementations if it doesn't satisfy reasonable engineering constraints, like efficiency, scalability, concurrency, latency variance, or strange resonances in the system (a significant performance issue in HPC). It is an optimization problem, not a correctness problem. If you applied the same systems solving methods to software as physical engineering, you should be able to predict system performance, concurrency, scaling, etc characteristics on a given hardware environment in concrete absolute terms without writing a line of code. The whole "build then measure" thing would be unnecessary. This is normal in physical engineering. I know software performance engineers that can predict these kinds of characteristics with surprising accuracy on a localized basis because they carry detailed system models in their heads, but that is a rare skill and to scale that up to a larger, more complex software system you really need some kind of automated solver. We use automated solvers in other engineering domains for the same reason -- human brains struggle to do this bit well.
- d0mine 2y ago
  Software is too complex to rely on predictions along. Predicting is useful but eventually you must measure. For example: "In conclusion, the issue isn't software-related. Python outperforms C/Rust due to an AMD CPU bug." https://xuanwo.io/2023/04-rust-std-fs-slower-than-python/#conclusion https://xuanwo.io/2023/04-rust-std-fs-slower-than-python/#co... Predict that.
  - ssivark 2y ago
    Predictions are always going to be limited by the world model they assume. Still useful in 99% of the cases.
    - d0mine 2y ago
      99% is hopelessly naive. If it were true, we would live in "generate code from UML" world (it is useful only for niche tasks)

by d0mine 2y ago

jandrewrogers 2y ago

These don't model key properties of software for systems engineering purposes. Software can be technically correct in a formal sense and also broken in all real implementations if it doesn't satisfy reasonable engineering constraints, like efficiency, scalability, concurrency, latency variance, or strange resonances in the system (a significant performance issue in HPC). It is an optimization problem, not a correctness problem. If you applied the same systems solving methods to software as physical engineering, you should be able to predict system performance, concurrency, scaling, etc characteristics on a given hardware environment in concrete absolute terms without writing a line of code. The whole "build then measure" thing would be unnecessary. This is normal in physical engineering. I know software performance engineers that can predict these kinds of characteristics with surprising accuracy on a localized basis because they carry detailed system models in their heads, but that is a rare skill and to scale that up to a larger, more complex software system you really need some kind of automated solver. We use automated solvers in other engineering domains for the same reason -- human brains struggle to do this bit well.

d0mine 2y ago
Software is too complex to rely on predictions along. Predicting is useful but eventually you must measure. For example: "In conclusion, the issue isn't software-related. Python outperforms C/Rust due to an AMD CPU bug." https://xuanwo.io/2023/04-rust-std-fs-slower-than-python/#conclusion https://xuanwo.io/2023/04-rust-std-fs-slower-than-python/#co... Predict that.
- ssivark 2y ago
  Predictions are always going to be limited by the world model they assume. Still useful in 99% of the cases.
  - d0mine 2y ago
    99% is hopelessly naive. If it were true, we would live in "generate code from UML" world (it is useful only for niche tasks)