5 ms·

In my opinion formal methods are what's missing from software engineering to make it a serious engineering discipline. In all other engineering fields you have

In my opinion formal methods are what's missing from software engineering to make it a serious engineering discipline. In all other engineering fields you have to produce calculations and "proofs" that your design ought to work. In software engineering everything is basically overcomplicated handwaving.

atoav 2y ago
> In software engineering everything is basically overcomplicated handwaving. No, it is worse than that. There are people who claim the proof is the code itself. Just look at it. These are the same kind of people claiming good code needs no documentation. That is like a bridge engineer saying they need no structural calculation because the stability of the bridge is obvious to a certain kind of bridge nerd if they look at it. Only that civil engineers figured out after a few high profile bridge collapses that "trust me bro" isn't good enough and software engineering people are still in the: "trust him, he is a genius"-phase of the field.
- mrkeen 2y ago
  > There are people who claim the proof is the code itself. Yet this is what emerges when you write a sufficiently detailed proof. The more detail you add to your TLA+ model, the more it looks like just another implementation (albeit untyped, so it's pretty easy to slip errors into).
  - szundi 2y ago
    We should have a TLA+^2 then. Oh the complexity has to be expressed anyway? Uh Oh and users mostly rather suffer from bugs than give up complex desires and features? Uh We’re doomed haha
    - atoav 2y ago
      Isn't that why we have modularization? In the end you can formally verify low level stuff on a per module basis. Knowing that your PNG decoder is formally verified and therefore it is less likely that a user uploads a PNG and gets Runtime Code Execution within that process context isn't worth nothing. And if it allows attackers to get RCE the number of mysterious crashes it might have produced with weird PNGs is probably also non-zero. In the end all security measures are a layered effort and doing a bit formal verification, a bit unit testing, a bit fuzzing etc. is always better than mentally aiming for 100% and not doing anything at all. The question regarding formal verification is: What is the code that is running in the critical domain? Someone who writes safe code will try to minimize the amount of code/executables/complexity in that space. And that domain isn't necessarily a single process, it can be a part in the code, or a process until it dropped privileges etc. If all your code is critical domain it either means you failed to sanitize inputs, everything runs with yolo/root privileges, all of your customers share a single table in your database, your hardcoded admin password is 1234 — or maybe you write code that controls nuclear power plants, airplanes or similar things. But if it is the former, no amount of formal verification will save you anyways because wrote software like a money writes poems: By accident. If the idea of a critical domain is new to those reading this comment, if you never thought about user proviledges when writing an application, please read this as proof of the point that the field of software engineering still lacks in all sort of places and it is in all our interest, both professional and as users/potential victims to improve the situation.
  - atoav 2y ago
    In the end, if you want the map to represent the landscape 100% you end up with another landscape. Granted. But engineering is about making sure we don't make mistakes and just like in math class a good way to assure that is to take two different paths and arrive at the same place.
ffsm8 2y ago
In theory, your software itself provides the proof that it does what it claims. The proof would directly link to unit tests or integration tests at the meta level. Arguably, software engineering does this much more exhaustively then any other engineering field... To very varying quality output, from masterpieces like SQLite to your average B2B artifact which barely works despite having 99% coverage.
- creshal 2y ago
  > In theory, your software itself provides the proof that it does what it claims. If you manage to solve the halting problem first.
  - seethedeaduu 2y ago
    People keep summoning the halting problem in unrelated contexts to handwave things awayvas impossible.
    - coldtea 2y ago
      Except in this case, where it's 100% fitting.
      - auggierose 2y ago
        It is only fitting if you think of providing the proof as a push button technology. That makes as much sense as thinking of providing the software itself as a push button technology.
        coldtea 2y ago
        It has nothing to do with the proof as a push button technology. Adding annotations to the code for example is not a workaround for the halting problem. (Working with a subset that's not-turing complete is, but that doesn't cover the general case the parent calls for, and is not practical with current software development languages and practices).
deleted 2y ago
[deleted]
vasco 2y ago
Software gets used for mission critical things all the time, with the same level of assuredness. What you are complaining about is that people making apps to show you the right advertisement or a website to watch pictures of cats sometimes is buggy and gets deployed without proper tests. Meanwhile almost every medical device under the sun today has software, nuclear powerplants run on software, space missions use software, airplanes drive themselves and land through software, etc.
- ethanwillis 2y ago
  It may be perceived that showing the right advertisements or showing pictures of cats isn't mission critical, and even just a toy. However, when massive amounts of personal information is being collected and shared by such applications I would say they're pretty important.
- davidgrenier 2y ago
  Your very last example kinda supports the thesis up there, considering how it's been going.
  - thebruce87m 2y ago
    Incredibly well, statistically?
  - hwayne 2y ago
    Notoriously, the 737 Max bug that killed a bunch of people was a software patch over a serious mechanical design flaw, and Boeing decided it was easier to make the software engineers fix it than redesign the entire plane.
ozim 2y ago
My opinion is that too many people think software engineering is not a serious engineering discipline and romanticize other engineering too much. For software that really matters you have standards like MISRA C you also have professional bodies like IEEE, ANSI, you have ISO standards for software development and infrastructure, there is a lot of standards and regulations that you can follow just like in all other fields. There is NIST for security and I could probably go on and on. So it is not "overcomplicated hand-waving". But no one is going to deal with "implementing formal approach" for "yet another crud app", they will hire whizz kid who knows latest JS framework and be done with it paying him 1/10th of cost of someone who knows more than that.
cubefox 2y ago
> In all other engineering fields you have to produce calculations and "proofs" that your design ought to work. That seems obviously false, unless you understand ""proof"" in such a lax manner that software engineering has them as well.
anal_reactor 2y ago
I was thinking about this, and to be honest, that's what I like about software. It needs to be a logical program, but there's also an artistic element to it. "Why did you name this variable like that? Because I was feeling like it"

atoav 2y ago

> In software engineering everything is basically overcomplicated handwaving. No, it is worse than that. There are people who claim the proof is the code itself. Just look at it. These are the same kind of people claiming good code needs no documentation. That is like a bridge engineer saying they need no structural calculation because the stability of the bridge is obvious to a certain kind of bridge nerd if they look at it. Only that civil engineers figured out after a few high profile bridge collapses that "trust me bro" isn't good enough and software engineering people are still in the: "trust him, he is a genius"-phase of the field.

mrkeen 2y ago
> There are people who claim the proof is the code itself. Yet this is what emerges when you write a sufficiently detailed proof. The more detail you add to your TLA+ model, the more it looks like just another implementation (albeit untyped, so it's pretty easy to slip errors into).
- szundi 2y ago
  We should have a TLA+^2 then. Oh the complexity has to be expressed anyway? Uh Oh and users mostly rather suffer from bugs than give up complex desires and features? Uh We’re doomed haha
  - atoav 2y ago
    Isn't that why we have modularization? In the end you can formally verify low level stuff on a per module basis. Knowing that your PNG decoder is formally verified and therefore it is less likely that a user uploads a PNG and gets Runtime Code Execution within that process context isn't worth nothing. And if it allows attackers to get RCE the number of mysterious crashes it might have produced with weird PNGs is probably also non-zero. In the end all security measures are a layered effort and doing a bit formal verification, a bit unit testing, a bit fuzzing etc. is always better than mentally aiming for 100% and not doing anything at all. The question regarding formal verification is: What is the code that is running in the critical domain? Someone who writes safe code will try to minimize the amount of code/executables/complexity in that space. And that domain isn't necessarily a single process, it can be a part in the code, or a process until it dropped privileges etc. If all your code is critical domain it either means you failed to sanitize inputs, everything runs with yolo/root privileges, all of your customers share a single table in your database, your hardcoded admin password is 1234 — or maybe you write code that controls nuclear power plants, airplanes or similar things. But if it is the former, no amount of formal verification will save you anyways because wrote software like a money writes poems: By accident. If the idea of a critical domain is new to those reading this comment, if you never thought about user proviledges when writing an application, please read this as proof of the point that the field of software engineering still lacks in all sort of places and it is in all our interest, both professional and as users/potential victims to improve the situation.
- atoav 2y ago
  In the end, if you want the map to represent the landscape 100% you end up with another landscape. Granted. But engineering is about making sure we don't make mistakes and just like in math class a good way to assure that is to take two different paths and arrive at the same place.

ffsm8 2y ago

In theory, your software itself provides the proof that it does what it claims. The proof would directly link to unit tests or integration tests at the meta level. Arguably, software engineering does this much more exhaustively then any other engineering field... To very varying quality output, from masterpieces like SQLite to your average B2B artifact which barely works despite having 99% coverage.

creshal 2y ago
> In theory, your software itself provides the proof that it does what it claims. If you manage to solve the halting problem first.
- seethedeaduu 2y ago
  People keep summoning the halting problem in unrelated contexts to handwave things awayvas impossible.
  - coldtea 2y ago
    Except in this case, where it's 100% fitting.
    - auggierose 2y ago
      It is only fitting if you think of providing the proof as a push button technology. That makes as much sense as thinking of providing the software itself as a push button technology.
      - coldtea 2y ago
        It has nothing to do with the proof as a push button technology. Adding annotations to the code for example is not a workaround for the halting problem. (Working with a subset that's not-turing complete is, but that doesn't cover the general case the parent calls for, and is not practical with current software development languages and practices).

deleted 2y ago

[deleted]

vasco 2y ago

Software gets used for mission critical things all the time, with the same level of assuredness. What you are complaining about is that people making apps to show you the right advertisement or a website to watch pictures of cats sometimes is buggy and gets deployed without proper tests. Meanwhile almost every medical device under the sun today has software, nuclear powerplants run on software, space missions use software, airplanes drive themselves and land through software, etc.

ethanwillis 2y ago
It may be perceived that showing the right advertisements or showing pictures of cats isn't mission critical, and even just a toy. However, when massive amounts of personal information is being collected and shared by such applications I would say they're pretty important.
davidgrenier 2y ago
Your very last example kinda supports the thesis up there, considering how it's been going.
- thebruce87m 2y ago
  Incredibly well, statistically?
- hwayne 2y ago
  Notoriously, the 737 Max bug that killed a bunch of people was a software patch over a serious mechanical design flaw, and Boeing decided it was easier to make the software engineers fix it than redesign the entire plane.

ozim 2y ago

My opinion is that too many people think software engineering is not a serious engineering discipline and romanticize other engineering too much. For software that really matters you have standards like MISRA C you also have professional bodies like IEEE, ANSI, you have ISO standards for software development and infrastructure, there is a lot of standards and regulations that you can follow just like in all other fields. There is NIST for security and I could probably go on and on. So it is not "overcomplicated hand-waving". But no one is going to deal with "implementing formal approach" for "yet another crud app", they will hire whizz kid who knows latest JS framework and be done with it paying him 1/10th of cost of someone who knows more than that.

cubefox 2y ago

> In all other engineering fields you have to produce calculations and "proofs" that your design ought to work. That seems obviously false, unless you understand ""proof"" in such a lax manner that software engineering has them as well.

anal_reactor 2y ago

I was thinking about this, and to be honest, that's what I like about software. It needs to be a logical program, but there's also an artistic element to it. "Why did you name this variable like that? Because I was feeling like it"