Now you’ve just shifted the problem to a much harder statement: proving the things the NN recognizes as a rose is actually a rose.

You cannot get rid of the enviroment, and the best thing you can do is be explicit in what you rely on. For example, formally verified operating systems often rely on hardware correctness, even though the errata sheets for modern CPUs are hundreds of pages long.

Just by reading the headlines I immediately suspected the topic of Verification vs Validation would be involved. I still cannot comprehend why it is still such a gap in many software projects I have worked in. Everyone knows about testing but barely a few understand or want to understand why Validation is equally important.

Yep... Along with this

Verification aligns with a specification. E.g. verify if what was implemented matches what was specified.

Validation aligns with a requirement. E.g. verify if what was implemented solves the actual problem.

While this is a good general rule of thumb, this terminology has nothing to do with how these terms are formally defined.

Verification first and foremost concerns design and development stage, a formal definition would be something like "outputs of design and development step meet specified requirements for that step". For example, you could verify that a formal specification for a module actually implements imposed requirements. Especially in software this can get murky as you cover different phases with different tests/suites, e.g. unit, integration, e2e implicitly test different stages, yet are often part of the same testing run.

Validation first and foremost concerns the whole system/product and fitness for market availability.

For example you would verify that e.g. for a motor vehicle ABS functions correctly, airbags deploy in a crash and frame meets passenger safety requirements in a crash, and you would still not be able to sell such vehicle. You would validate the vehicle as a whole with corresponding regulatory body to get vehicle deemed fit for market.

TLDR: Verification is getting passing grade in a lab test, validation is submitting all relevant lab test protocols to get CE certified.

There is an important and distinct pair of definitions used by a possibly smaller but significant number of people:

Verification: formal theoretical proof

Validation: Empirical test based approach

If it's hard to remember which is which, maybe they should be different words.

Like "Customer validation" and "Verification against the spec"

Like "sympathy" and "empathy". I finally heard a mnemonic but if I need a mnemonic maybe it's a sign that the words are just too hard to understand

Should we validate before we verify the software?

Nit: ">"

No assumption holds for all environments.

Posh example: Axiom of choice.

This is why one would prefer to run. NGINX over a formally verified http server.

It's not a substitute, an assertion only makes sure that it doesn't happen unnoticed, a proof says that it doesn't happen at all. I might prefer to know that my reactor control system has no overflow ahead of time, rather than getting an assertion and crashing if it happens (though it would be a bad reactor control system if it couldn't handle crashes).

Nearly everything that goes wrong for me in prod is already a crash/stacktrace, which is what an assertion does.

The point of proofs is to not get yourself (or the customer) into that point in the first place.

I think other responses here may miss an important line of thought.

There seems to be confusion around the differences between bug and correct.

In the referenced study on binary searches, the Google researchers stated that most implementations had bugs AND were "broken" because they did:

    int mid =(low + high) / 2;

Ostensibly, a proof may require mid to be positive at all times and therefore be invalid because of overflow.

The question is: if we put in assertions everywhere that guarantee correct output, where aborting on overflow is considered correct, then are folks going to say that's correct, or are they going to say oh that's not what binary search is so you haven't implemented it?

EDIT: thinking about it more, it seems that null must be an accepted output of any program due to the impossibility of representing very large numbers.

Correct. You wouldn't prove everything in a typical production system unless that system is controlling a rocket or a pacemaker.

You may want to prove some things. Test others.

Types are proofs by the way. Most programmers find that handy.

I think assertions are rediculously underused BTW

If you're flying a plane, you probably don't want safety critical code to throw an assertion. It's for this reason that Airbus spends a bunch of money & time on proving their flight control software.

Better to use a type which cannot represent an invalid state.

For example, instead of defining `inc` with `Int`s, the equivalent of an `IncrementalInt` type parameter for the `inc` function will ensure correctness without requiring runtime assertions.

By "asserting X" do you mean "checking whether X is true and crashing the program if not", like the assert macro in C or the assert statement in Python? No, that is almost never done, for three reasons:

• Crashing the program is often what you formally verified the program to prevent in the first place! A crashing program is what destroyed Ariane 5 on its maiden flight, for example. Crashing the program is often the worst possible outcome rather than an acceptable one.

• Many of the assumptions are not things that a program can check are true. Examples from the post include "nothing is concurrently modifying [variables]", "the compiler worked correctly, the hardware isn't faulty, and the OS doesn't mess with things," and, "unsafe [Rust] code does not have [a memory bug] either." None of these assumptions could be reliably verified by any conceivable test a program could make.

• Even when the program could check an assumption, it often isn't computationally feasible; for example, binary search of an array is only valid if the array is sorted, but checking that every time the binary search routine is invoked would take it from logarithmic time to linear time, typically an orders-of-magnitude slowdown that would defeat the purpose of using a binary search instead of a simpler sequential search. (I think Hillel tried to use this example in the article but accidentally wrote "binary sort" instead, which isn't a thing.)

When crashing the program is acceptable and correctness preconditions can be efficiently checked, postconditions usually can be too. In those cases, it's common to use either runtime checks or property-based testing instead of formal verification, which is harder.

That’s impractical. Take binary search and the assumption the list is sorted. Verifying the list is sorted would negate the point of binary search as you would be inspecting every item in the list.

How would that look like if you accidentally assumed you have arbitrary large integers but in practice you have 64 bits?

They do if they’re in the specs. See near-universal use of lockstep processors, ECC etc in safety-critical and high radiation cases, which comes from the two requirements that “a single bit flip from a cosmic ray shall be detectable” and “multiple simultaneous hit flips from cosmic rays shall be shown to be sufficiently rare in the operating environment.”

Specifications that are formally verified can definitely cover real-time guarantees, behaviour under error returns from operations like allocation, and similar things. Hardware failures can be accounted for in hardware verification, which is much like software verification: specification + hardware design = verified design; if the spec covers it, the verification guarantees it.

Considering software alone isn't pretty useless, nor is having the guarantee that "inc x = x - 1" will always go from an Int to an Int, even if it's not "fully right" at least trying to increment a string or a complex number will be rejected at compile time. Giving up on any improvements in the correctness of code because it doesn't get you all the way to 100% correct is, IMO, defeatist.

(Giving up on it because it has diminishing returns and isn't worth the effort is reasonable, of course!)

Nowhere does the article claim that:

   "formal verification of the code" -> "high integrity system"

Now, if you want to formally verify your program can tolerate any number of bits flip on any variables at any moment(s) in time, it will happily test this for you. Unfortunately, assuming presently known software methods, this is an unmeetable specification :)

Even then you have other physical issues to consider. This is one of the things I love about the Space Shuttle. It had 5 computers for redundancy during launch and return. You obviously don't want to put them all in the same place so you spread them out among the avionics bays. You also obviously don't want them all installed in the same orientation so you install them differently with respect to the vehicles orientation. You also have a huge data network that requires redundancy and you take all the same steps with the multiplexers as well.

For portable libraries and apps, there's only so much you can do. However, there are some interesting properties you can prove assuming the environment behaves according to a spec.

The article does consider hardware failure, yes.

Side channels? Is best out of 2 sufficient or is best out of 3 necessary?

From https://news.ycombinator.com/context?id=39938759 re: s2n-tls:

> [ FizzBee, Nagini, Deal-solver, Dafny; icontract, pycontracts, Hoare logic, DbC Design-by-Contract, invariants, parallelism and concurrency and locks, io latency, pass by reference in distributed systems, "FaCT: A DSL for Timing-Sensitive Computation" and side channels [in hw and software] https://news.ycombinator.com/item?id=38527663 ]

There are so many things to consider;

/? awesome-safety https://westurner.github.io/hnlog/#search:awesome-safety :

awesome-safety-critical: https://awesome-safety-critical.readthedocs.io/en/latest/

Hazard (logic) https://en.wikipedia.org/wiki/Hazard_(logic)

Hazard (computer architecture); out-of-order execution and delays: https://en.wikipedia.org/wiki/Hazard_(computer_architecture)

Soft error: https://en.wikipedia.org/wiki/Soft_error

SEU: Single-Event Upset: https://en.wikipedia.org/wiki/Single-event_upset

And then cosmic ray and particle physics