7 ms·

I work in formal verification at a FAANG. It is so wildly more expensive than traditional development that it is simply not feasible to apply it anywhere but a

I work in formal verification at a FAANG. It is so wildly more expensive than traditional development that it is simply not feasible to apply it anywhere but absolutely the most critical paths, and even then, the properties asserted by formal verification are often quite a bit less powerful than necessary to truly guarantee something useful. I want formal verification everywhere. I believe in provable correctness. I wish we could hire people capable of always writing software to that standard and maintaining those proofs alongside their work. We really can’t, though. Its a frustrating reality of being human — we know how to do it better, but nearly all of even the smartest engineers we can hire are not smart enough.

jacquesm 11mo ago
Ok, let's start off with holding them to the same standards as avionics software development. The formal verification can wait.
- frumplestlatz 11mo ago
  Agreed. I left out any commentary on `.unwrap()` from my original comment, but it’s an obvious example of something that should never have appeared in critical code.
  - echelon 11mo ago
    Rust needs to get rid of .unwrap() and its kin. They're from pre-1.0 Rust, before many of the type system features and error handling syntax sugar were added. There's no reason to use them as the language provides lots of safer alternatives. If you do want to trigger a panic, you can, but I'd also ask - why? Alternatively, and perhaps even better, Rust needs a way to mark functions that can panic for any reason other than malloc failures. Any function that then calls a panicky function needs to be similarly marked. In doing this, we can statically be certain no such methods are called if we want to be rid of the behavior. Perhaps something like: panic fn my_panicky_function() { None.unwrap(); // NB: `unwrap()` is also marked `panic` in stdlib } fn my_safe_function() { // with a certain compiler or Crates flag, this would fail to compile // as my_safe_function isn't annotated as `panic` my_panicky_function() } The ideal future would be to have code that is 100% panic free.
    - jacquesm 11mo ago
      I'd say the equivalent of Erlang's supervisor trees is what is needed but once you go that route you might as well use Erlang.
      - ViewTrick1002 11mo ago
        Or just deploy containers with an orchestrator restarting them when failing? It is not like an Erlang service would be able to make progress with an invalid config either.
        lenkite 11mo ago
        What happens when they "keep" failing ? You never get to know what is causing your nightmare.
        jacquesm 11mo ago
        That's fair, but even there the roll-back would be a lot smoother, besides the supervisor trees are a lot more fine grained than restarting entire containers when they fail.
      - zbentley 11mo ago
        I’m not sure that panic (speaking generally about the majority of its uses and the spirit of the law; obviously 100% of code does not obey this) is the equivalent of an Erlang process crash in most cases. Rather, I think unwrap()/panic are usually used in ways more similar to erlang:halt/1.
        jacquesm 11mo ago
        Exactly, but that is kind of the point here. An Erlang 'halt' is something that most Erlang programmers would twig is not what you want in most cases, in most cases you want your process to crash and for the supervisor to restart it if the error is recoverable. What happened here is systemic: the config file contained an issue severe enough that it precluded the system from running in the first place and unfortunately that caused a runtime error when in fact that validation should have been separate from the actual use. This is where I see the problem with this particular outage. And that makes it an engineering issue much more than a language issue. Bad configuration files can and do happen, so you take that eventuality into account during systems design.
  - antonvs 11mo ago
    And it's so easy to avoid, as well. #![deny(clippy::unwrap_used)] or cargo clippy -- -D clippy::unwrap_used Put that in your CI pipeline, and voila. Global crash averted.
  - lenkite 11mo ago
    ON HN, just a couple of years ago, a famous Rust programmer said that it is OK to use unwrap. Rustaceans supported this position. Cloudflare merely followed the community standard. Using unwrap() in Rust is Okay https://news.ycombinator.com/item?id=32385102 https://news.ycombinator.com/item?id=32385102 https://burntsushi.net/unwrap/ https://burntsushi.net/unwrap/
    - deleted 11mo ago
      [deleted]
    - burntsushi 11mo ago
      I already had a conversation with the GP specifically: https://news.ycombinator.com/item?id=45979127 https://news.ycombinator.com/item?id=45979127 They aren't presenting a coherent philosophy. And when asked for examples, or to engage directly with examples in my blog, they can't or won't do it. But yes, of course it's okay to use unwrap(). It's just an assertion. Assertions are fine.
      - frumplestlatz 11mo ago
        Result declares a type-level invariant — an assertion enforced by the compiler, not runtime — that the operation can fail. Ignoring that is bypassing the type system. It means your types are either wrong, or your type system is incapable of modeling your true invariants. In the case of the cloudflare error, their types were wrong. That was an avoidable failure. They needed to fix their type-level invariants, not yolo the issue with `.unwrap()`. Your willful persistent lack of understanding doesn’t mean my philosophy is incoherent. Using `.unwrap()` is always an example of a failure to accurately model your invariants in the type system.
        burntsushi 11mo ago
        Your definition of "correct" is completely incoherent. Just because an invariant that could be modeled by a type system is not modeled by the type system in any given scenario does not make it incorrect. You can't engage with my examples and you provide none of your own. So continuing discussion with you is a waste of time.
  - deleted 11mo ago
    [deleted]
- robocat 11mo ago
  Anyone in avionics software dev to give an opinion? I would presume there's the same issue as parent said: It is so wildly more expensive than traditional development that it is simply not feasible to apply it anywhere but absolutely the most critical paths
  - jacquesm 11mo ago
    > Anyone in avionics software dev to give an opinion? I've done some for fuel estimation of freighter jets (not quite avionics but close enough to get a sense for the development processes) and the amount of rigor involved in that one project made me a better developer for the rest of my career. Was it slow? Yes, it was very slow. A couple of thousand lines of code, a multiple of that in tests for a very long time compare to what it would normally take me. But within the full envelope of possible inputs it performed exactly as advertised. The funny thing is that I'm not particularly proud of it, it was the process that kept things running even when my former games programmer mentality would have long ago said 'ship it'. Some things you just need to do properly, or not at all.
  - vel0city 11mo ago
    Compare the prices for type certified parts on aircraft compared to comparable (but not proven) similar parts in the automotive space. Its crazy how much more expensive actually proving these parts perform to spec to the level required by aviation law. It wouldn't surprise me to find doing the same kind of certifications for complex avionics software to be the same.
- dpark 11mo ago
  I don’t understand why anyone should want this. Why should normal engineering efforts be held to the same standards as life-critical systems? Why would anyone expect that CloudFlare DDoS protection be built to the standards of avionics equipment? Also if we’re being fair, avionics software is far narrower in scope than just “software in general”. And even with that Boeing managed to kill a bunch of people with shitty software.
  - jacquesm 11mo ago
    > I don’t understand why anyone should want this. That's ok, but then you should bow out of the conversation, which is between people that do understand why anyone should want this. To have predictable behavior is a must have in some industries, less in others. At the level of infrastructure that is deemed critical by some - and I'm curious what JGC's position on this is - the ability to avoid this kind of outage carries a lot of value. The fact that you do not see that CF has achieved life-critical reach is one that tells me that most of this effort is probably going to waste, but I trust that John does see it my way and realizes that if there are ways to avoid these kind of issues they should be researched. Because service uptime is something very important to companies like Cloudflare. Boeing managed to kill a bunch of people with shitty business practices, not with shitty software, the software did what it was built to do. It is the whole process around that software as well as the type certification process and regulatory oversight that failed dramatically.
    - dpark 11mo ago
      > That's ok, but then you should bow out of the conversation, which is between people that do understand why anyone should want this. I was not making a statement that I am ignorant. I was saying I believe the proposal to model general software engineering after avionics is misguided and inviting you to clarify your position. It is certainly valid to ask what CloudFlare or anyone else for that matter could learn from avionics engineering or from NASA or from civil engineering focused on large scale projects or anywhere else that good engineering practices might come from. However, there is a persistent undercurrent in discussions around software reliability and general software engineering that ignore the fact that there are major trade-offs made for different engineering efforts. “Oh, look how reliable avionics are. We should just copy that.” Cool, except I would bet avionics cost 100 times as much to build per line of code as anything CloudFlare has ever shipped. The design constraints are just fundamentally different. Avionics are built for a specific purpose in an effectively unchanging environment. If Cloudflare built their offerings in the same way, they would never ship new features, the quality of their request filtering would plummet as adversaries adjusted faster than CloudFlare could react, and realistically they would be overtaken by a competitor within a few years at most. They aren’t building avionics, so they shouldn’t engineer as if they are. Their engineering practices should reflect the reality of the environment in which they are building a product. This is no different than people who ask, “Why don’t we build software the way we build bridges?” Because we’re not building bridges. Most bridges look exactly like some other bridge that was built 10 miles away. That’s nothing like building new software. That’s far more like deploying a new instance of existing software with slightly different config. And this is not to say that there is nothing for software engineers to learn from bridge building, but reductive “just do it like them” thinking is not useful. > Boeing managed to kill a bunch of people with shitty business practices, not with shitty software, the software did what it was built to do. The software was poorly designed. No doubt it was implemented the spec. Does that change the fact that the sum total of the engineering yielded a deadly result? There is no papering over the fact that “building to avionics standards” led direct to the deaths of 346 people in this case.
- khuey 11mo ago
  Are Cloudflare's customers willing to pay avionics software level prices?
  - jacquesm 11mo ago
    Given that Cloudflare's market cap is 1/2 of Boeing's and they are not making a physical product I would say: Clearly, yes.
    - vntok 11mo ago
      The vast majority of Cloudflare's "customers" are paying 0 to 20 dollars a month, for virtually the same protection coverage and features as most of their 200 dollars/mo customers. That's not remotely in the realm of avionics price structure, be it software or hardware.
      - jacquesm 11mo ago
        It is the aggregate they pay that counts here, not the individual payments. A better comparison would be to compare this to airline passengers paying for their tickets, they pay a few hundred bucks in the expectation that they will arrive at their destination. Besides, it is not the customers that determine Cloudflare's business model, Cloudflare does. Note that their whole business is to prevent outages and that as soon as they become the cause of an outage they have invalidated their whole reason for existence. Of course you could then turn this into a statistical argument that as long as they prevent more outages than they cause that they are a net benefit but that's not what this discussion is about, it is first and foremost about the standard of development they are held up against. Ericsson identified similar issues in their offering long ago and created a very capable solution and I'm wondering if that would not have been a better choice for this kind of project, even if it would have resulted in more resource consumption.
        dpark 11mo ago
        > as soon as they become the cause of an outage they have invalidated their whole reason for existence This is a bar no engineering effort has ever met. “If you ever fail, even for a moment, there’s no reason for you to even exist.” There have been 6 fatal passenger airplane crashes in the US this year alone. NASA only built 6 shuttles and 2 of those exploded, killing their crews. And these were life-preserving systems that failed. Discussions around software engineering quality always seem to veer into spaces where we assign almost mythic properties to other engineering efforts in an attempt to paint software engineering as lazy or careless.
ottah 11mo ago
I would argue the largest CDN provider in the world is a critical path.
- rdtsc 11mo ago
  I would guess at the individual team level they probably still behave like any other tech shop. When the end of the year comes the higher-ups still expect fancy features and accomplishments and saying "well, we spent months writing a page of TLA+ code" is not going to look as "flashy" as another team who delivered 20 new features. It would take someone from above to push and ask that other team who delivered 20 features, where is their TLA+ code verifying their correctness. But, how many people in the middle management chain would do that?
dpark 11mo ago
> we know how to do it better, but nearly all of even the smartest engineers we can hire are not smart enough. This seems like a contradiction. If the smartest engineers you can hire are not smart enough to work within formal verification constraints then we in fact do not know how to do this. If formal verification hinges on having perfect engineers then it’s useless because perfect engineers wouldn’t need formal verification.
- frumplestlatz 11mo ago
  > If formal verification hinges on having perfect engineers then it’s useless because perfect engineers wouldn’t need formal verification. It doesn’t hinge on having perfect engineers. It hinges on engineers being able to model problems algebraically and completely, prove the equivalence of multiple such models at different layers of abstraction (including equivalence to the original code), and then prove that useful properties hold across those models.
  - dpark 11mo ago
    If the smartest engineers cannot do it, it doesn’t work. This isn’t even getting to the practical question of whether it’s worth doing, given the significant additional cost. If the smartest folks you can find are not smart enough to use the framework then it’s useless. Maybe this means the tooling is insufficient. Maybe it means the field isn’t mature enough. Whatever, if you need an IQ two standard deviations above normal and 10x as long it’s not real world useable today.
    - Nevermark 11mo ago
      > If the smartest engineers cannot do it, it doesn’t work. [FIX:] ..., it doesn't work universally. And the answer to that is pretty clear. It does not work universally. If every developer started only shipping code they had credibly formally verified, the vast majority of developers would go into shock at the scale of work to be done. Even the best "validators" would fall into career shredding pits, due to "minor" but now insurmountable dependencies in previously unverified projects. The vast majority of projects would go into unrecoverable stalls. But formal validation can still work some of the time with the right people, on the right scale and kind of project, with the right amount of resources/time expended. It isn't as if regular "best practices" programming works universally either. But validation is much harder.
lenkite 11mo ago
We need modern programming languages with formal verification built-in - should be applicable to specially demarcated functions/modules. It is a headache to write TLA+ and keep the independent spec up2date with the productive code.
jacquesm 11mo ago
The big trick is - as far as I understand it - to acknowledge that systems fail and to engineer for dealing with those failures. I support your efforts downthread for at least knowing whether or not underlying abstractions are able to generate a panic (which is a massive side effect) or are only able to return valid results or error flags. The higher level the abstraction the bigger the chance that there is a module somewhere in the stack that is able to blow it all up, at the highest level you can pretty much take it as read that this is the case. So unless you engineer the whole thing from the ground up without any library modules it is impossible to guarantee that this is not the case and as far as I understand your argument you at least want to be informed when that is the case, or, alternatively, to cause the compiler to flag the situation down from your code as incompatible with the guarantees that you are asking for, is that a correct reading?
gavinhoward 11mo ago
Hey, where can I apply to a job like yours? I may not be smart enough, but I may be. And I am very interested in formal verification.

jacquesm 11mo ago

Ok, let's start off with holding them to the same standards as avionics software development. The formal verification can wait.

frumplestlatz 11mo ago
Agreed. I left out any commentary on `.unwrap()` from my original comment, but it’s an obvious example of something that should never have appeared in critical code.
- echelon 11mo ago
  Rust needs to get rid of .unwrap() and its kin. They're from pre-1.0 Rust, before many of the type system features and error handling syntax sugar were added. There's no reason to use them as the language provides lots of safer alternatives. If you do want to trigger a panic, you can, but I'd also ask - why? Alternatively, and perhaps even better, Rust needs a way to mark functions that can panic for any reason other than malloc failures. Any function that then calls a panicky function needs to be similarly marked. In doing this, we can statically be certain no such methods are called if we want to be rid of the behavior. Perhaps something like: panic fn my_panicky_function() { None.unwrap(); // NB: `unwrap()` is also marked `panic` in stdlib } fn my_safe_function() { // with a certain compiler or Crates flag, this would fail to compile // as my_safe_function isn't annotated as `panic` my_panicky_function() } The ideal future would be to have code that is 100% panic free.
  - jacquesm 11mo ago
    I'd say the equivalent of Erlang's supervisor trees is what is needed but once you go that route you might as well use Erlang.
    - ViewTrick1002 11mo ago
      Or just deploy containers with an orchestrator restarting them when failing? It is not like an Erlang service would be able to make progress with an invalid config either.
      - lenkite 11mo ago
        What happens when they "keep" failing ? You never get to know what is causing your nightmare.
      - jacquesm 11mo ago
        That's fair, but even there the roll-back would be a lot smoother, besides the supervisor trees are a lot more fine grained than restarting entire containers when they fail.
    - zbentley 11mo ago
      I’m not sure that panic (speaking generally about the majority of its uses and the spirit of the law; obviously 100% of code does not obey this) is the equivalent of an Erlang process crash in most cases. Rather, I think unwrap()/panic are usually used in ways more similar to erlang:halt/1.
      - jacquesm 11mo ago
        Exactly, but that is kind of the point here. An Erlang 'halt' is something that most Erlang programmers would twig is not what you want in most cases, in most cases you want your process to crash and for the supervisor to restart it if the error is recoverable. What happened here is systemic: the config file contained an issue severe enough that it precluded the system from running in the first place and unfortunately that caused a runtime error when in fact that validation should have been separate from the actual use. This is where I see the problem with this particular outage. And that makes it an engineering issue much more than a language issue. Bad configuration files can and do happen, so you take that eventuality into account during systems design.
- antonvs 11mo ago
  And it's so easy to avoid, as well. #![deny(clippy::unwrap_used)] or cargo clippy -- -D clippy::unwrap_used Put that in your CI pipeline, and voila. Global crash averted.
- lenkite 11mo ago
  ON HN, just a couple of years ago, a famous Rust programmer said that it is OK to use unwrap. Rustaceans supported this position. Cloudflare merely followed the community standard. Using unwrap() in Rust is Okay https://news.ycombinator.com/item?id=32385102 https://news.ycombinator.com/item?id=32385102 https://burntsushi.net/unwrap/ https://burntsushi.net/unwrap/
  - deleted 11mo ago
    [deleted]
  - burntsushi 11mo ago
    I already had a conversation with the GP specifically: https://news.ycombinator.com/item?id=45979127 https://news.ycombinator.com/item?id=45979127 They aren't presenting a coherent philosophy. And when asked for examples, or to engage directly with examples in my blog, they can't or won't do it. But yes, of course it's okay to use unwrap(). It's just an assertion. Assertions are fine.
    - frumplestlatz 11mo ago
      Result declares a type-level invariant — an assertion enforced by the compiler, not runtime — that the operation can fail. Ignoring that is bypassing the type system. It means your types are either wrong, or your type system is incapable of modeling your true invariants. In the case of the cloudflare error, their types were wrong. That was an avoidable failure. They needed to fix their type-level invariants, not yolo the issue with `.unwrap()`. Your willful persistent lack of understanding doesn’t mean my philosophy is incoherent. Using `.unwrap()` is always an example of a failure to accurately model your invariants in the type system.
      - burntsushi 11mo ago
        Your definition of "correct" is completely incoherent. Just because an invariant that could be modeled by a type system is not modeled by the type system in any given scenario does not make it incorrect. You can't engage with my examples and you provide none of your own. So continuing discussion with you is a waste of time.
- deleted 11mo ago
  [deleted]
robocat 11mo ago
Anyone in avionics software dev to give an opinion? I would presume there's the same issue as parent said: It is so wildly more expensive than traditional development that it is simply not feasible to apply it anywhere but absolutely the most critical paths
- jacquesm 11mo ago
  > Anyone in avionics software dev to give an opinion? I've done some for fuel estimation of freighter jets (not quite avionics but close enough to get a sense for the development processes) and the amount of rigor involved in that one project made me a better developer for the rest of my career. Was it slow? Yes, it was very slow. A couple of thousand lines of code, a multiple of that in tests for a very long time compare to what it would normally take me. But within the full envelope of possible inputs it performed exactly as advertised. The funny thing is that I'm not particularly proud of it, it was the process that kept things running even when my former games programmer mentality would have long ago said 'ship it'. Some things you just need to do properly, or not at all.
- vel0city 11mo ago
  Compare the prices for type certified parts on aircraft compared to comparable (but not proven) similar parts in the automotive space. Its crazy how much more expensive actually proving these parts perform to spec to the level required by aviation law. It wouldn't surprise me to find doing the same kind of certifications for complex avionics software to be the same.
dpark 11mo ago
I don’t understand why anyone should want this. Why should normal engineering efforts be held to the same standards as life-critical systems? Why would anyone expect that CloudFlare DDoS protection be built to the standards of avionics equipment? Also if we’re being fair, avionics software is far narrower in scope than just “software in general”. And even with that Boeing managed to kill a bunch of people with shitty software.
- jacquesm 11mo ago
  > I don’t understand why anyone should want this. That's ok, but then you should bow out of the conversation, which is between people that do understand why anyone should want this. To have predictable behavior is a must have in some industries, less in others. At the level of infrastructure that is deemed critical by some - and I'm curious what JGC's position on this is - the ability to avoid this kind of outage carries a lot of value. The fact that you do not see that CF has achieved life-critical reach is one that tells me that most of this effort is probably going to waste, but I trust that John does see it my way and realizes that if there are ways to avoid these kind of issues they should be researched. Because service uptime is something very important to companies like Cloudflare. Boeing managed to kill a bunch of people with shitty business practices, not with shitty software, the software did what it was built to do. It is the whole process around that software as well as the type certification process and regulatory oversight that failed dramatically.
  - dpark 11mo ago
    > That's ok, but then you should bow out of the conversation, which is between people that do understand why anyone should want this. I was not making a statement that I am ignorant. I was saying I believe the proposal to model general software engineering after avionics is misguided and inviting you to clarify your position. It is certainly valid to ask what CloudFlare or anyone else for that matter could learn from avionics engineering or from NASA or from civil engineering focused on large scale projects or anywhere else that good engineering practices might come from. However, there is a persistent undercurrent in discussions around software reliability and general software engineering that ignore the fact that there are major trade-offs made for different engineering efforts. “Oh, look how reliable avionics are. We should just copy that.” Cool, except I would bet avionics cost 100 times as much to build per line of code as anything CloudFlare has ever shipped. The design constraints are just fundamentally different. Avionics are built for a specific purpose in an effectively unchanging environment. If Cloudflare built their offerings in the same way, they would never ship new features, the quality of their request filtering would plummet as adversaries adjusted faster than CloudFlare could react, and realistically they would be overtaken by a competitor within a few years at most. They aren’t building avionics, so they shouldn’t engineer as if they are. Their engineering practices should reflect the reality of the environment in which they are building a product. This is no different than people who ask, “Why don’t we build software the way we build bridges?” Because we’re not building bridges. Most bridges look exactly like some other bridge that was built 10 miles away. That’s nothing like building new software. That’s far more like deploying a new instance of existing software with slightly different config. And this is not to say that there is nothing for software engineers to learn from bridge building, but reductive “just do it like them” thinking is not useful. > Boeing managed to kill a bunch of people with shitty business practices, not with shitty software, the software did what it was built to do. The software was poorly designed. No doubt it was implemented the spec. Does that change the fact that the sum total of the engineering yielded a deadly result? There is no papering over the fact that “building to avionics standards” led direct to the deaths of 346 people in this case.
khuey 11mo ago
Are Cloudflare's customers willing to pay avionics software level prices?
- jacquesm 11mo ago
  Given that Cloudflare's market cap is 1/2 of Boeing's and they are not making a physical product I would say: Clearly, yes.
  - vntok 11mo ago
    The vast majority of Cloudflare's "customers" are paying 0 to 20 dollars a month, for virtually the same protection coverage and features as most of their 200 dollars/mo customers. That's not remotely in the realm of avionics price structure, be it software or hardware.
    - jacquesm 11mo ago
      It is the aggregate they pay that counts here, not the individual payments. A better comparison would be to compare this to airline passengers paying for their tickets, they pay a few hundred bucks in the expectation that they will arrive at their destination. Besides, it is not the customers that determine Cloudflare's business model, Cloudflare does. Note that their whole business is to prevent outages and that as soon as they become the cause of an outage they have invalidated their whole reason for existence. Of course you could then turn this into a statistical argument that as long as they prevent more outages than they cause that they are a net benefit but that's not what this discussion is about, it is first and foremost about the standard of development they are held up against. Ericsson identified similar issues in their offering long ago and created a very capable solution and I'm wondering if that would not have been a better choice for this kind of project, even if it would have resulted in more resource consumption.
      - dpark 11mo ago
        > as soon as they become the cause of an outage they have invalidated their whole reason for existence This is a bar no engineering effort has ever met. “If you ever fail, even for a moment, there’s no reason for you to even exist.” There have been 6 fatal passenger airplane crashes in the US this year alone. NASA only built 6 shuttles and 2 of those exploded, killing their crews. And these were life-preserving systems that failed. Discussions around software engineering quality always seem to veer into spaces where we assign almost mythic properties to other engineering efforts in an attempt to paint software engineering as lazy or careless.

ottah 11mo ago

I would argue the largest CDN provider in the world is a critical path.

rdtsc 11mo ago
I would guess at the individual team level they probably still behave like any other tech shop. When the end of the year comes the higher-ups still expect fancy features and accomplishments and saying "well, we spent months writing a page of TLA+ code" is not going to look as "flashy" as another team who delivered 20 new features. It would take someone from above to push and ask that other team who delivered 20 features, where is their TLA+ code verifying their correctness. But, how many people in the middle management chain would do that?

dpark 11mo ago

> we know how to do it better, but nearly all of even the smartest engineers we can hire are not smart enough. This seems like a contradiction. If the smartest engineers you can hire are not smart enough to work within formal verification constraints then we in fact do not know how to do this. If formal verification hinges on having perfect engineers then it’s useless because perfect engineers wouldn’t need formal verification.

frumplestlatz 11mo ago
> If formal verification hinges on having perfect engineers then it’s useless because perfect engineers wouldn’t need formal verification. It doesn’t hinge on having perfect engineers. It hinges on engineers being able to model problems algebraically and completely, prove the equivalence of multiple such models at different layers of abstraction (including equivalence to the original code), and then prove that useful properties hold across those models.
- dpark 11mo ago
  If the smartest engineers cannot do it, it doesn’t work. This isn’t even getting to the practical question of whether it’s worth doing, given the significant additional cost. If the smartest folks you can find are not smart enough to use the framework then it’s useless. Maybe this means the tooling is insufficient. Maybe it means the field isn’t mature enough. Whatever, if you need an IQ two standard deviations above normal and 10x as long it’s not real world useable today.
  - Nevermark 11mo ago
    > If the smartest engineers cannot do it, it doesn’t work. [FIX:] ..., it doesn't work universally. And the answer to that is pretty clear. It does not work universally. If every developer started only shipping code they had credibly formally verified, the vast majority of developers would go into shock at the scale of work to be done. Even the best "validators" would fall into career shredding pits, due to "minor" but now insurmountable dependencies in previously unverified projects. The vast majority of projects would go into unrecoverable stalls. But formal validation can still work some of the time with the right people, on the right scale and kind of project, with the right amount of resources/time expended. It isn't as if regular "best practices" programming works universally either. But validation is much harder.

lenkite 11mo ago

We need modern programming languages with formal verification built-in - should be applicable to specially demarcated functions/modules. It is a headache to write TLA+ and keep the independent spec up2date with the productive code.

jacquesm 11mo ago

The big trick is - as far as I understand it - to acknowledge that systems fail and to engineer for dealing with those failures. I support your efforts downthread for at least knowing whether or not underlying abstractions are able to generate a panic (which is a massive side effect) or are only able to return valid results or error flags. The higher level the abstraction the bigger the chance that there is a module somewhere in the stack that is able to blow it all up, at the highest level you can pretty much take it as read that this is the case. So unless you engineer the whole thing from the ground up without any library modules it is impossible to guarantee that this is not the case and as far as I understand your argument you at least want to be informed when that is the case, or, alternatively, to cause the compiler to flag the situation down from your code as incompatible with the guarantees that you are asking for, is that a correct reading?

gavinhoward 11mo ago

Hey, where can I apply to a job like yours? I may not be smart enough, but I may be. And I am very interested in formal verification.