4 ms·

I don't think formal verification really addresses most day-to-day programming problems: * A user interface is confusing, or the English around it is uncle

I don't think formal verification really addresses most day-to-day programming problems: * A user interface is confusing, or the English around it is unclear * An API you rely on changes, is deprecated, etc. * Users use something in unexpected ways * Updates forced by vendors or open source projects cause things to break * The customer isn't clear what they want * Complex behavior between interconnected systems, out of the purview of the formal language (OS + database + network + developer + VM + browser + user + web server) For some mathematically pure task, sure, it's great. Or a low-level library like a regular expression parser or a compression codec. But I don't think that represents a lot of what most of us are tasked with, and those low-level "mathematically pure" libraries are generally pretty well handled by now.

adrianN 10mo ago
TBH most day to day programming problems are barely worth having tests for. But if we had formal specs and even just hand wavy correspondences between the specs and the implementation for the low level things everybody depends on that would be a huge improvement for the reliability of the whole ecosystem.
gizmo686 10mo ago
A limited form of formal verification is already mainstream. It is called type systems. The industry in general has been slowly moving to encode more invariants into the type system, because every invariant that is in the type system is something you can stop thinking about until the type checker yells at you. A lot of libraries document invariants that are either not checked at all, only at runtime, or somewhere in between. For instance, the requirement that a collection not be modified during interaction. Or that two region of memory do not overlap, or that a variable is not modified without owning a lock. These are all things that, in principle, can be formally verified. No one claims that good type systems prevent buggy software. But, they do seem to improve programmer productivity. For LLMs, there is an added benefit. If you can formally specify what you want, you can make that specification your entire program. Then have an LLM driven compiler produce a provably correct implementation. This is a novel programming paradigm that has never before been possible; although every "declarative" language is an attempt to approximate it.
- devin 10mo ago
  > No one claims that good type systems prevent buggy software. But, they do seem to improve programmer productivity. They really don’t. How did you arrive at such a conclusion?
  - mplewis 10mo ago
    Through empirical evidence? Do you think that the vast majority of software devs moved to typing for no reason?
    - avmich 10mo ago
      It's a bad reason. A lot of best practices are temporary blindnesses, comparable, in some sense, with supposed love to BASIC before or despite Dijkstra. So, yes, it's possible there is no good reason. Though I don't think it's the case here.
    - wolvesechoes 10mo ago
      > Do you think that the vast majority of software devs moved to typing for no reason? It is quite clear that this industry is mostly driven by hype and fades, not by empirical studies. Empirical evidence in favor of a claim that static typing and complex type systems reduce bugs or improve productivity is highly inconclusive at best
    - gf000 10mo ago
      We don't actually have empirical evidence on the topic, surprisingly. It's just people's hunches.
      - JumpCrisscross 10mo ago
        I feel like the terms logical, empirical, rational and objective are used interchangeably by the general public, with one being in vogue at a time.
  - Permik 10mo ago
est 10mo ago
> An API you rely on changes, is deprecated, etc Formal verification will eventually lead to good, stable API design. > Users use something in unexpected ways > Complex behavior between interconnected systems It happens when there's no formal verification during the design stage. Formal verification literally means cover 100% state changes and for every possible input/output, every execution branch should be tested.
- Joker_vD 10mo ago
  > Formal verification will eventually lead to good, stable API design. Why? Has it ever happened like this? Because to me it would seem that if the system verified to work, then it works no matter how API is shaped, so there is no incentive to change it to something better.
  - est 10mo ago
    > if the system verified to work, then it works no matter how API is shaped That's the case for one-off integrations, but the messy part always comes when system goal changes Let's say formal verification could help to avoid some anti-patterns.
    - Joker_vD 10mo ago
      > Let's say formal verification could help to avoid some anti-patterns. I'd still like to hear about the actual mechanism of this happening. Because I personally find it much easier to believe that the moment keeping the formal verification up to date becomes untenable for whatever reason (specs changing too fast, external APIs to use are too baroque, etc) people would rather say "okay, guess we ditch the formal verification and just keep maintaining the integration tests" instead of "let's change everything about the external world so we could keep our methodology".
      - est 10mo ago
        > I'd still like to hear about the actual mechanism of this happening I am not an expert on this, but the worst API I've seen is those with hidden states. e.g. .toggle() API. Call it old number of times, it goes to one state, call it even number of times, it goes back. And there's call A before you call B types of APIs, the client has to keep a strict call order (which itself is a state machine of some kind)
Byamarro 10mo ago
In fact, automated regression tests done by ai with visual capabilities may have bigger impact than formal verification has. You can have an army of testers now, painfully going through every corner of your software
- petesergeant 10mo ago
  In practice ends up being a bit like static analysis though, which is you get a ton of false positives. All said, I’m now running all commits through Codex (which is the only thing it’s any good at), and it’s really pretty good at code reviews.
- Maxion 10mo ago
  Will only work somewhat when customers expect features to work in a standard way. When customer spec things to work in non-standard approaches you'll just end up with a bunch of false positives.
  - MetaWhirledPeas 10mo ago
    This. When the bugs come streaming in you better have some other AI ready to triage them and more AI to work them, because no human will be able to keep up with it all. Bug reporting is already about signal vs noise. Imagine how it will be when we hand the megaphone to bots.
ErroneousBosh 10mo ago
> But I don't think that represents a lot of what most of us are tasked with Give me a list of all the libraries you work with that don't have some sort of "okay but not that bit" rule in the business logic, or "all of those function are f(src, dst) but the one you use most is f(dst,src) and we can't change it now". I bet it's a very short list. Really we need to scrap every piece of software ever written and start again from scratch with all these weirdities written down so we don't do it again, but we never will.
- bluGill 10mo ago
  Scrapping everything wouldn't help. 15 years ago the project I'm on did that - for a billion dollars. We fixed the old mistakes but made plenty of new ones along the way. We are trying to fix those now and I can't help but wonder what new mistakes we are making the in 15 years we will regret.
  - ErroneousBosh 10mo ago
    Computers are terrible and software is terrible and we should just go back to tilling the fields with horses and drinking beer.
wolfgangbabad 10mo ago
Yeah, there were about 5 or 10 videos about this "complexity" and unpredictability of 3rd parties and wheels involved that AI doesn't control and even forget - small context window - in like past few weeks. I am sure you have seen at least one of them ;) But it's true. AI is still super narrow and dumb. Don't understand basic prompts even. Look at the computer games now - they still don't look real despite almost 30 years since Half-life 1 started the revolution - I would claim. Damn, I think I ran it on 166 Mhz computer on some lowest details even. Yes, it's just better and better but still looking super uncanny - at least to me. And it's been basically 30 years of constant improvements. Heck, Roomba is going bankrupt. I am not saying things don't improve but the hype and AI bubble is insane and the reality doesn't match the expectation and predictions at all.
raxxorraxor 10mo ago
That has been the problem with unit and integration tests all the time. Especially for systems that tend to be distributed. AI makes creating mock objects much easier in some cases, but it still creates a lot of busy work and makes configuration more difficult. At at this points it often is difficult configuration management that cause the issues in the first place. Putting everything in some container doesn't help either, on the contrary.
nwah1 10mo ago
> Complex behavior between interconnected systems, out of the purview of the formal language (OS + database + network + developer + VM + browser + user + web server) Isn't this what TLA+ was meant to deal with?
- skydhash 10mo ago
  Not really, some components like components have a lot of properties that’s very difficult to modelize. Take latency in network, or storage performance in OS.
ScottBurson 10mo ago
Actually, formal verification could help massively with four of those problems — all but the first (UI/UX) and fifth (requirements will always be hard). A change in the API of a dependency should be detected immediately and handled silently. Reliance on unspecified behavior shouldn't happen in the first place; the client's verification would fail. Detecting breakage caused by library changes should be where verification really shines; when you get the update, you try to re-run your verification, and if that fails, it tells you what the problem is. As for interconnected systems, again, that's pretty much the whole point. Obviously, achieving this dream will require formalizing pretty much everything, which is well beyond our capabilities now. But eventually, with advances in AI, I think it will be possible. It will take something fundamentally better than today's LLMs, though.

adrianN 10mo ago

TBH most day to day programming problems are barely worth having tests for. But if we had formal specs and even just hand wavy correspondences between the specs and the implementation for the low level things everybody depends on that would be a huge improvement for the reliability of the whole ecosystem.

gizmo686 10mo ago

A limited form of formal verification is already mainstream. It is called type systems. The industry in general has been slowly moving to encode more invariants into the type system, because every invariant that is in the type system is something you can stop thinking about until the type checker yells at you. A lot of libraries document invariants that are either not checked at all, only at runtime, or somewhere in between. For instance, the requirement that a collection not be modified during interaction. Or that two region of memory do not overlap, or that a variable is not modified without owning a lock. These are all things that, in principle, can be formally verified. No one claims that good type systems prevent buggy software. But, they do seem to improve programmer productivity. For LLMs, there is an added benefit. If you can formally specify what you want, you can make that specification your entire program. Then have an LLM driven compiler produce a provably correct implementation. This is a novel programming paradigm that has never before been possible; although every "declarative" language is an attempt to approximate it.

devin 10mo ago
> No one claims that good type systems prevent buggy software. But, they do seem to improve programmer productivity. They really don’t. How did you arrive at such a conclusion?
- mplewis 10mo ago
  Through empirical evidence? Do you think that the vast majority of software devs moved to typing for no reason?
  - avmich 10mo ago
    It's a bad reason. A lot of best practices are temporary blindnesses, comparable, in some sense, with supposed love to BASIC before or despite Dijkstra. So, yes, it's possible there is no good reason. Though I don't think it's the case here.
  - wolvesechoes 10mo ago
    > Do you think that the vast majority of software devs moved to typing for no reason? It is quite clear that this industry is mostly driven by hype and fades, not by empirical studies. Empirical evidence in favor of a claim that static typing and complex type systems reduce bugs or improve productivity is highly inconclusive at best
  - gf000 10mo ago
    We don't actually have empirical evidence on the topic, surprisingly. It's just people's hunches.
    - JumpCrisscross 10mo ago
      I feel like the terms logical, empirical, rational and objective are used interchangeably by the general public, with one being in vogue at a time.
- Permik 10mo ago

est 10mo ago

> An API you rely on changes, is deprecated, etc Formal verification will eventually lead to good, stable API design. > Users use something in unexpected ways > Complex behavior between interconnected systems It happens when there's no formal verification during the design stage. Formal verification literally means cover 100% state changes and for every possible input/output, every execution branch should be tested.

Joker_vD 10mo ago
> Formal verification will eventually lead to good, stable API design. Why? Has it ever happened like this? Because to me it would seem that if the system verified to work, then it works no matter how API is shaped, so there is no incentive to change it to something better.
- est 10mo ago
  > if the system verified to work, then it works no matter how API is shaped That's the case for one-off integrations, but the messy part always comes when system goal changes Let's say formal verification could help to avoid some anti-patterns.
  - Joker_vD 10mo ago
    > Let's say formal verification could help to avoid some anti-patterns. I'd still like to hear about the actual mechanism of this happening. Because I personally find it much easier to believe that the moment keeping the formal verification up to date becomes untenable for whatever reason (specs changing too fast, external APIs to use are too baroque, etc) people would rather say "okay, guess we ditch the formal verification and just keep maintaining the integration tests" instead of "let's change everything about the external world so we could keep our methodology".
    - est 10mo ago
      > I'd still like to hear about the actual mechanism of this happening I am not an expert on this, but the worst API I've seen is those with hidden states. e.g. .toggle() API. Call it old number of times, it goes to one state, call it even number of times, it goes back. And there's call A before you call B types of APIs, the client has to keep a strict call order (which itself is a state machine of some kind)

Byamarro 10mo ago

In fact, automated regression tests done by ai with visual capabilities may have bigger impact than formal verification has. You can have an army of testers now, painfully going through every corner of your software

petesergeant 10mo ago
In practice ends up being a bit like static analysis though, which is you get a ton of false positives. All said, I’m now running all commits through Codex (which is the only thing it’s any good at), and it’s really pretty good at code reviews.
Maxion 10mo ago
Will only work somewhat when customers expect features to work in a standard way. When customer spec things to work in non-standard approaches you'll just end up with a bunch of false positives.
- MetaWhirledPeas 10mo ago
  This. When the bugs come streaming in you better have some other AI ready to triage them and more AI to work them, because no human will be able to keep up with it all. Bug reporting is already about signal vs noise. Imagine how it will be when we hand the megaphone to bots.

ErroneousBosh 10mo ago

> But I don't think that represents a lot of what most of us are tasked with Give me a list of all the libraries you work with that don't have some sort of "okay but not that bit" rule in the business logic, or "all of those function are f(src, dst) but the one you use most is f(dst,src) and we can't change it now". I bet it's a very short list. Really we need to scrap every piece of software ever written and start again from scratch with all these weirdities written down so we don't do it again, but we never will.

bluGill 10mo ago
Scrapping everything wouldn't help. 15 years ago the project I'm on did that - for a billion dollars. We fixed the old mistakes but made plenty of new ones along the way. We are trying to fix those now and I can't help but wonder what new mistakes we are making the in 15 years we will regret.
- ErroneousBosh 10mo ago
  Computers are terrible and software is terrible and we should just go back to tilling the fields with horses and drinking beer.

wolfgangbabad 10mo ago

Yeah, there were about 5 or 10 videos about this "complexity" and unpredictability of 3rd parties and wheels involved that AI doesn't control and even forget - small context window - in like past few weeks. I am sure you have seen at least one of them ;) But it's true. AI is still super narrow and dumb. Don't understand basic prompts even. Look at the computer games now - they still don't look real despite almost 30 years since Half-life 1 started the revolution - I would claim. Damn, I think I ran it on 166 Mhz computer on some lowest details even. Yes, it's just better and better but still looking super uncanny - at least to me. And it's been basically 30 years of constant improvements. Heck, Roomba is going bankrupt. I am not saying things don't improve but the hype and AI bubble is insane and the reality doesn't match the expectation and predictions at all.

raxxorraxor 10mo ago

That has been the problem with unit and integration tests all the time. Especially for systems that tend to be distributed. AI makes creating mock objects much easier in some cases, but it still creates a lot of busy work and makes configuration more difficult. At at this points it often is difficult configuration management that cause the issues in the first place. Putting everything in some container doesn't help either, on the contrary.

nwah1 10mo ago

> Complex behavior between interconnected systems, out of the purview of the formal language (OS + database + network + developer + VM + browser + user + web server) Isn't this what TLA+ was meant to deal with?

skydhash 10mo ago
Not really, some components like components have a lot of properties that’s very difficult to modelize. Take latency in network, or storage performance in OS.

ScottBurson 10mo ago

Actually, formal verification could help massively with four of those problems — all but the first (UI/UX) and fifth (requirements will always be hard). A change in the API of a dependency should be detected immediately and handled silently. Reliance on unspecified behavior shouldn't happen in the first place; the client's verification would fail. Detecting breakage caused by library changes should be where verification really shines; when you get the update, you try to re-run your verification, and if that fails, it tells you what the problem is. As for interconnected systems, again, that's pretty much the whole point. Obviously, achieving this dream will require formalizing pretty much everything, which is well beyond our capabilities now. But eventually, with advances in AI, I think it will be possible. It will take something fundamentally better than today's LLMs, though.