Comment by mensetmanusman

In theory, yeah. In many ways that's what test driven development is, you keep breaking down a problem into a function that you can write a unit test for, write the test, write the implementation, move on. In practice writing the functions and verifying their inputs and outputs isn't the hard bit.

The hard bit is knowing which functions to write, and what "valid" means for inputs and outputs. Sometimes you'll get a specification that tells you this, but the moment you try to implement it you'll find out that whoever was writing that spec didn't really think it through to its conclusion. There will be a host of edge cases that probably don't matter, and will probably never be hit in the real world anyway, but someone needs to make that call and decide what to do when (not if) they get hit anyway.

Not without extraordinary cost that no one (save NASA, perhaps) is willing to pay.

Even if you can formally verify individual methods, what you're actually looking for is if we can verify systems. Because systems, even ones made of of pieces that are individually understood, have interactions and emergent behaviors which are not expected.

Pretty much, yes. But what i think you’re talking about (formal verification of code) is a bit of a dark art and barely makes it out of very specialised stuff like warhead guidance computers and maybe some medical stuff etc.

In theory you cannot even say for all programs and all inputs if the program will finish the calculation [0]. In practice you often can break it down but the number of combinations of input is what makes it impossible to test everything. Most developers try to keep individual functions as small as possible to understand them easier. You can use math to do formal verification, but that gets difficult with real programs too.

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

What you're describing is basically perfect unit testing. There was even a trend called TDD ( test driven development ) that tried to make the tests the driving force behind building the software in the first place. It works but it has to be perfect and, inevitably, your tests need testing and so you're back to square one. Regardless, it's tedious and time consuming and shortcuts get taken then value of the whole thing falls apart and running the unit tests just becomes like a ritual with no real meaning/impact.

No, it is not possible, not only in practice but - more importantly - in theory as well:

https://pron.github.io/posts/correctness-and-complexity

functional code because it intentionally always takes input and returns output. However not all code is functional and testing has a side effect of making change harder. So if you write a lot of half-useless tests that break when you change anything then you've just made your code harder to change. Even with an AI doing that automatically the damage is contextual, which tests should be removed after a given change and which kept? It requires a decent amount of thought.

Outside of functional code, there's a lot out there which requires mutable state. This is much harder to test which is why user interface testing on native apps is always more painful and most people still run manual QA or use an entirely different testing approach.

Long story short: no.

Long story: yes, but it'd take centuries to verify all possible inputs, at least for any non-trivial programs.

There are many implications to this question! TLDR; in theory yes, in practice no.

Can a function be "verified", this can mean "tested", "reviewed", "proved to be correct". What does correct even mean?

Functions in code are often more complex than just having input and output, unlike mathematical functions. Very often, they have side effects, like sending packets on network or modifying things in their environment. This makes it difficult to understand what they do in isolation.

Any non-trivial piece of software is almost impossible to fully understand or test. These things work empirically and require constant maintenance and tweaking.

Not really.

If a program is built with strong software architecture, then a lot of it will fit that definition. As an analogy, electricity in your home is delivered by electrical outlets that are standardized -- you can have high confidence that when you buy a new electrical appliance, it can plug into those outlets and work. But someone had to design that standard and apply it universally to the outlets and the appliances. Software architecture within a program is about creating those standards on how things work and applying them universally. If you do this well, then yes, you can have a lot of code that is testable and verifiable.

But you'll always have side-effects. Programs do things -- they create files, they open network connections, they communicate with other programs, they display things on the screen. Some of those side-effects create "state" -- once a file is created, it's still present. These things are much harder to test because they're not just a function with an input and an output -- their behavior changes between the first run and the second run.

No. Not every program can be broken down so. If you want that kind of certainty, this consideration needs to be part of the development process from the very beginning. This is what functional programming is all about.