3 ms·

This is overblown imo. of all of the areas/domains where this might be an issue, programming isn't it. Programs run. if they work as envisioned then you're good

This is overblown imo. of all of the areas/domains where this might be an issue, programming isn't it. Programs run. if they work as envisioned then you're good to go. and in numerous other professions, nobody is signing off work that hasn't been checked by multiple parties either way, LLMs will be a pipeline in this process.

skydhash 4y ago
Happy paths and edge cases. The computer view of the world is very rigid. Most of the effort spent on programming, IMO, is coming up with solutions to handle all the way the algorithm could fail, especially when dealing with inputs and outputs. The great thing about research is having a much wider view of the problem and the surrounding context. Generating a solution with LLMs is like looking through a window instead of climbing on the roof.
- nextaccountic 4y ago
  > Happy paths and edge cases. That's what model checkers are for, right? Here's a recent post about this https://model-checking.github.io/kani-verifier-blog/2023/03/31/how-kani-helped-find-bugs-in-hifitime.html https://model-checking.github.io/kani-verifier-blog/2023/03/... > Kani has helped fix at least eight different categories of bugs in a single pull request: https://github.com/nyx-space/hifitime/pull/192 https://github.com/nyx-space/hifitime/pull/192. Most of these were bugs near the boundaries of a Duration definition: around the zero, maximum, and minimum durations. But many of the bugs were on important and common operations: partial equality, negation, addition, and subtraction operations. These bugs weren’t due to lax testing: there are over 74 integration tests with plenty of checks within each. > One of the great features of Kani is that it performs what is known as symbolic execution of programs, where inputs are modelled as symbolic variables covering whole ranges of values at once. All program behaviors possible under these inputs are analyzed for defects like arithmetic overflows or underflows, signed conversion overflow or underflow, etc. If a defect is possible for some values of the inputs, Kani will generate a counter example trace with concrete values triggering the defect. > Thanks to how Kani analyzes a program, tests can either have explicit post-conditions or not. A test with explicit post-conditions includes an assertion: execute a set of instructions and then check something. This is a typical test case. > Kani can also test code where there is no explicit condition to check. Instead, only the successive operations of a function call are executed, and each are tested by Kani for failure cases by analyzing the inputs and finding cases where inputs will lead to runtime errors like overflows. This approach is how most of the bugs in hifitime have been found. I expect that in some decades LLMs will be able to leverage this kind of stuff
hn_go_brrrrr 4y ago
Therac-25 would tend to disagree with you.

skydhash 4y ago

Happy paths and edge cases. The computer view of the world is very rigid. Most of the effort spent on programming, IMO, is coming up with solutions to handle all the way the algorithm could fail, especially when dealing with inputs and outputs. The great thing about research is having a much wider view of the problem and the surrounding context. Generating a solution with LLMs is like looking through a window instead of climbing on the roof.

nextaccountic 4y ago
> Happy paths and edge cases. That's what model checkers are for, right? Here's a recent post about this https://model-checking.github.io/kani-verifier-blog/2023/03/31/how-kani-helped-find-bugs-in-hifitime.html https://model-checking.github.io/kani-verifier-blog/2023/03/... > Kani has helped fix at least eight different categories of bugs in a single pull request: https://github.com/nyx-space/hifitime/pull/192 https://github.com/nyx-space/hifitime/pull/192. Most of these were bugs near the boundaries of a Duration definition: around the zero, maximum, and minimum durations. But many of the bugs were on important and common operations: partial equality, negation, addition, and subtraction operations. These bugs weren’t due to lax testing: there are over 74 integration tests with plenty of checks within each. > One of the great features of Kani is that it performs what is known as symbolic execution of programs, where inputs are modelled as symbolic variables covering whole ranges of values at once. All program behaviors possible under these inputs are analyzed for defects like arithmetic overflows or underflows, signed conversion overflow or underflow, etc. If a defect is possible for some values of the inputs, Kani will generate a counter example trace with concrete values triggering the defect. > Thanks to how Kani analyzes a program, tests can either have explicit post-conditions or not. A test with explicit post-conditions includes an assertion: execute a set of instructions and then check something. This is a typical test case. > Kani can also test code where there is no explicit condition to check. Instead, only the successive operations of a function call are executed, and each are tested by Kani for failure cases by analyzing the inputs and finding cases where inputs will lead to runtime errors like overflows. This approach is how most of the bugs in hifitime have been found. I expect that in some decades LLMs will be able to leverage this kind of stuff

hn_go_brrrrr 4y ago

Therac-25 would tend to disagree with you.