Reliable Software in the LLM Era(quint-lang.org) |
Reliable Software in the LLM Era(quint-lang.org) |
Basically AI now makes every product operate as if it has a vibrant open-source community with hundreds of contributions per day and a small core team with limited capacity.
It just changes in terms of doubling the work you have to do in order verify your system rather than you writing the code from scratch, because you have to figure out whatever code your AI agent spitted out before beginning the formal verification process.
With you having written the code from scratch, you already know it beforehand and the verification process is more smoother.
A more concrete example is maybe you have tests that show you put a highlight on the active item tests that show you don’t put the highlight on the inactive items, but with an llm you might also want to have tests that wait a while and verify the highlight is not flickering on and off overtime (something so absurd you wouldn’t even test for it before AI).
The value of these test is in catching areas of the code where things are drifting towards nonsense because humans aren’t reviewing as thoroughly. I don’t think that you can realistically have 100% data coverage and prevent every single bug and not review the code. It’s just that I found that slightly more tests are warranted if you do want to step back.
Hmm this is an interesting analogy. It suggests that we could design autonomous AI coding scaffold tools based on the patterns found in open source development communities.
I hope this is a tongue in cheek jab at how AI writes prose, because Claude loves to prefix lines with this.
It's true what they say that it is easy to make a demo in AI, but super hard to turn demo into some product or thing other people can use. We are trying :) but also, most posts I read on this topic are just philosophical and give absolutely nothing you can learn and use. We are trying to provide concrete ideas on the things we are exploring, like in our newest post: https://quint-lang.org/posts/cognitive_debt
I'm also a bit happy you see some sales drive in that post since I'm 100% technical and trying to be more sales-inclined. I'm learning to find the balance. If it helps, it's more like I'm so extremely hyped about this and want to convince people to use it. And everything we built so far is open source, so it's really about selling the cool idea of formal methods at this point.
TL;DR: I feel like my time is being wasted when I read AI-written articles, so I stop reading. Do with my anecdote what you will!
Can we settle on Slop Decade?
"Spectacle is an embedded domain-specific language that provides a family of type-level combinators for authoring specifications of program behavior along with a model checker for verifying that user implementations of a program satisfy written specifications."
It's in Haskell, but...
For the second post, it was a wall of prose that my colleague, Josef, wrote (I'm pretty sure without AI). I added the more concrete example sections and then asked AI to suggest some heading names to break down the prose, and I'm assuming this was my mistake as the headings are the first thing people read and AI loves headings. I always broke down text in headings before AI, this suck haha.
Anyway, I'll definitely increase my neurotic levels about this. It's not worth at all to rush things if it will make the post more empty to read in any way.
As for Hitchen's razor, when it does apply, it applies implicitly, with no need for a comment or explicit mention.
It is not "bullshit" as you said it, since no real argument was made that it is. Hitchen's razor applies to your claim.
I doubt that. My engagement with HN is on a level of morbid curiosity bordering on naked disdain. If n-gate was still a thing I probably would have quit checking the site altogether some years ago.