3 ms·

Most people don't bother with formal verification because it costs extra labor and time. LLMs address both. I've been enjoying working with an LLM on Rust pro

Most people don't bother with formal verification because it costs extra labor and time. LLMs address both. I've been enjoying working with an LLM on Rust projects, especially for writing tests, which aren't the same as formal verification, but it's in the same ballpark.

cryptonym 1y ago
Vibe-coding tests is nowhere near formal verification.
- timschmidt 1y ago
  When typewriters spread in the late 19th century, clerks who used them were sometimes called “mechanical scribblers” or accused of doing “machine work” rather than proper clerical labor. When adding machines and calculators appeared in offices, detractors claimed they would weaken the mind. In the mid-20th century, some educators derided calculator users as “button pushers” rather than “real mathematicians.” In the 1980s, early adopters of personal computers and word processors were sometimes called “typists with toys.” Secretaries who mastered word processors were sometimes derided as “not real secretaries” because they lacked shorthand or dictation skills. Architects and engineers who switched from drafting tables to CAD in the 1970s–80s faced accusations that CAD work was “cookie-cutter” and lacked craftsmanship. Traditional draftsmen argued that “real” design required hand drawing, while CAD users were seen as letting the machine think for them. Across history, the insults usually follow the same structure: - Suggesting the new tool makes the work too easy, therefore less valuable. - Positioning users as “operators” rather than “thinkers.” - Romanticizing the older skill as more “authentic” or “serious.”
  - cryptonym 1y ago
    Few generated unit tests doesn't replace formal verification. That's just not the same thing at all, it's not a matter of manual vs automated calculator.
    - timschmidt 1y ago
      > Few generated unit tests doesn't replace formal verification. That's a claim you're making for the first time, here. Not one I've made. Go ahead and re-read my comments to verify.
drdrey 1y ago
not even close to being in the same ballpark
- timschmidt 1y ago
  Let me know when you find a memory error or concurrency problem, or really any undefined behavior in any of my code.
  - Disposal8433 1y ago
    > https://github.com/timschmidt/repsnapper/blob/master/src/shape.h#L150 https://github.com/timschmidt/repsnapper/blob/master/src/sha... That variable is undefined in multiple constructors. Also your code cannot compile in various scenarios. Have a nice day.
    - cyberpunk 1y ago
      It's been 5 days and I'm still laughing about this one. Bravo.
      - timschmidt 1y ago
        I'm laughing too, that code is 13 years old, committed by hurzl here: https://github.com/timschmidt/repsnapper/commit/5410b5d278a5338ed9820811fe693618b5c59304 https://github.com/timschmidt/repsnapper/commit/5410b5d278a5... and in C++. To be clear, I'd handed off maintainership at least a decade ago. I haven't touched this software in many years. Just noticed the reply. So this doesn't seem relevant to the conversation about LLMs, Rust, and software quality improvement methods from strict typing to formal verification. It's like a "gotcha!" that didn't land. Sorry. Please, find some bugs in a project I've touched in the last few years! Looking for things to fix. Please open a github issue from an account linked to your projects next time so I can return the favor :D The bugs are in there, I know they are, but with an LLM and a bit of time to review it's work, it now costs me a few minutes tops to write a test to exclude future cases of the same problem or class of problems. Which is a level of verification beyond what's been allocated time in previous projects, where the tests never got written or very infrequently. Repsnapper's a great example of that. We didn't have a standardized testing framework we were using across the dozen or so libraries we'd integrated into the app. The original author Kulitorum sort of copied and pasted bits and pieces of code together to write the app originally, without much concern for licenses or origin tracking, so I initiated a line-by-line audit and license verification for the codebase in order to qualify it for inclusion in Fedora and Debian to make 3D printing easier and more available as there were no printing tools shipping in a distro at the time. Integrating new libraries into that codebase was unpleasant, working with the build system in general was not my favorite. Lots of room to screw it up, but it has to be just right to work. I think having llms and a testing framework would have allowed us to evolve the Repsnapper code a lot more safely, and a lot further than we ever managed. Well, and I can say that pretty safely now that I'm in the process of doing just that with https://github.com/timschmidt/alumina-firmware https://github.com/timschmidt/alumina-firmware and https://github.com/timschmidt/alumina-ui https://github.com/timschmidt/alumina-ui and https://github.com/timschmidt/csgrs https://github.com/timschmidt/csgrs They're all still very young, still some things stubbed out, code is gross pending revision and cleanup, but it's basically Repsnapper 3.0 in Rust but this version includes CAD and a motion control firmware and fits in < 4mb. Among them I already have hundreds of tests entirely absent from Repsnapper. Couldn't have written csgrs without them. Probably a lot of redundant tests at this point, as things have changed rapidly. I'm only about 6mo of effort in.

cryptonym 1y ago

Vibe-coding tests is nowhere near formal verification.

timschmidt 1y ago
When typewriters spread in the late 19th century, clerks who used them were sometimes called “mechanical scribblers” or accused of doing “machine work” rather than proper clerical labor. When adding machines and calculators appeared in offices, detractors claimed they would weaken the mind. In the mid-20th century, some educators derided calculator users as “button pushers” rather than “real mathematicians.” In the 1980s, early adopters of personal computers and word processors were sometimes called “typists with toys.” Secretaries who mastered word processors were sometimes derided as “not real secretaries” because they lacked shorthand or dictation skills. Architects and engineers who switched from drafting tables to CAD in the 1970s–80s faced accusations that CAD work was “cookie-cutter” and lacked craftsmanship. Traditional draftsmen argued that “real” design required hand drawing, while CAD users were seen as letting the machine think for them. Across history, the insults usually follow the same structure: - Suggesting the new tool makes the work too easy, therefore less valuable. - Positioning users as “operators” rather than “thinkers.” - Romanticizing the older skill as more “authentic” or “serious.”
- cryptonym 1y ago
  Few generated unit tests doesn't replace formal verification. That's just not the same thing at all, it's not a matter of manual vs automated calculator.
  - timschmidt 1y ago
    > Few generated unit tests doesn't replace formal verification. That's a claim you're making for the first time, here. Not one I've made. Go ahead and re-read my comments to verify.

drdrey 1y ago

not even close to being in the same ballpark

timschmidt 1y ago
Let me know when you find a memory error or concurrency problem, or really any undefined behavior in any of my code.
- Disposal8433 1y ago
  > https://github.com/timschmidt/repsnapper/blob/master/src/shape.h#L150 https://github.com/timschmidt/repsnapper/blob/master/src/sha... That variable is undefined in multiple constructors. Also your code cannot compile in various scenarios. Have a nice day.
  - cyberpunk 1y ago
    It's been 5 days and I'm still laughing about this one. Bravo.
    - timschmidt 1y ago
      I'm laughing too, that code is 13 years old, committed by hurzl here: https://github.com/timschmidt/repsnapper/commit/5410b5d278a5338ed9820811fe693618b5c59304 https://github.com/timschmidt/repsnapper/commit/5410b5d278a5... and in C++. To be clear, I'd handed off maintainership at least a decade ago. I haven't touched this software in many years. Just noticed the reply. So this doesn't seem relevant to the conversation about LLMs, Rust, and software quality improvement methods from strict typing to formal verification. It's like a "gotcha!" that didn't land. Sorry. Please, find some bugs in a project I've touched in the last few years! Looking for things to fix. Please open a github issue from an account linked to your projects next time so I can return the favor :D The bugs are in there, I know they are, but with an LLM and a bit of time to review it's work, it now costs me a few minutes tops to write a test to exclude future cases of the same problem or class of problems. Which is a level of verification beyond what's been allocated time in previous projects, where the tests never got written or very infrequently. Repsnapper's a great example of that. We didn't have a standardized testing framework we were using across the dozen or so libraries we'd integrated into the app. The original author Kulitorum sort of copied and pasted bits and pieces of code together to write the app originally, without much concern for licenses or origin tracking, so I initiated a line-by-line audit and license verification for the codebase in order to qualify it for inclusion in Fedora and Debian to make 3D printing easier and more available as there were no printing tools shipping in a distro at the time. Integrating new libraries into that codebase was unpleasant, working with the build system in general was not my favorite. Lots of room to screw it up, but it has to be just right to work. I think having llms and a testing framework would have allowed us to evolve the Repsnapper code a lot more safely, and a lot further than we ever managed. Well, and I can say that pretty safely now that I'm in the process of doing just that with https://github.com/timschmidt/alumina-firmware https://github.com/timschmidt/alumina-firmware and https://github.com/timschmidt/alumina-ui https://github.com/timschmidt/alumina-ui and https://github.com/timschmidt/csgrs https://github.com/timschmidt/csgrs They're all still very young, still some things stubbed out, code is gross pending revision and cleanup, but it's basically Repsnapper 3.0 in Rust but this version includes CAD and a motion control firmware and fits in < 4mb. Among them I already have hundreds of tests entirely absent from Repsnapper. Couldn't have written csgrs without them. Probably a lot of redundant tests at this point, as things have changed rapidly. I'm only about 6mo of effort in.