On: New fuzzing tool finds USB bugs in Linux, Windows, macOS, and FreeBSD

[MaxBarraclough]

So the machinist had been using rigorous testing, catching all defects prior to release, rather than using a correct-by-construction methodology. Either approach seems fine.

[bluGill → MaxBarraclough]

Neither is perfect. Tests are only as good as your imagination of what to test. Proof by construction is only as good as your ability to have the right axioms

[MaxBarraclough → bluGill]

> Tests are only as good as your imagination of what to test.

A lot of work has been done on code-coverage, boundary-analysis, etc. Testing can never be complete, though.

> Proof by construction is only as good as your ability to have the right axioms

That's not a good summary of the challenges that formal methods face with respect to correctness. Defects can creep in at various points.

See p. 46 of the PDF linked from https://www.adacore.com/tokeneer

[monadic2 → MaxBarraclough]

Well, apparently it didn’t catch the defect that mattered. Typical engineer trying to justify an engineering mistake!

[hawski → MaxBarraclough]

He never had problem with use-after-free, because he was leaking memory.