[flagged]
Reliable Software in the LLM Era
21–30 of 39 posts
Re: Reliable Software in the LLM Era
#22Earlier quoted context omitted.
Shallow dismissals are not permitted on this site as per its rules.
Not everything is worthy of a 5000 word Atlantic-style deconstruction when presented. I think the community largely embraces Hitchens' Razor. That being the case what is the minimum word count required to issue a dismissal?
Please. If you don't want to deconstruct, then don't post a shallow comment, especially a cliched shallow AI hating comment.
As for Hitchen's razor, when it does apply, it applies implicitly, with no need for a comment or explicit mention.
Re: Reliable Software in the LLM Era
#23Nothing changes in terms of how to make reliable software. You need the same things like unit tests, integration tests, monitoring tools, etc. 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.
> Nothing changes in terms of how to make reliable software. You need the same things like unit tests, integration tests, monitoring tools, etc.
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.
Re: Reliable Software in the LLM Era
#24I haven't even used TLA+ yet and now it's got derivatives... My understanding is: TLA+ but like C, functional, and typed.
https://hackage.haskell.org/package/spectacle
"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...
Re: Reliable Software in the LLM Era
#25Re: Reliable Software in the LLM Era
#26Re: Reliable Software in the LLM Era
#27AI Era, Agentic Era, LLM Era... Can we settle on Slop Decade?
I like Macroslop because it pokes fun at the company who dislikes their new pet name so much they ban people for using it
Re: Reliable Software in the LLM Era
#28> But here’s the hopeful part:
I hope this is a tongue in cheek jab at how AI writes prose, because Claude loves to prefix lines with this.
Re: Reliable Software in the LLM Era
#29I haven't even used TLA+ yet and now it's got derivatives... My understanding is: TLA+ but like C, functional, and typed.
TLA+ is around 30 years old.
Re: Reliable Software in the LLM Era
#30The idea is interesting, but have some more respect for your potential readers and actually write the post. There’s so much AI sales drivel here it’s hard to see what’s interesting about your product. I’m more interested in the choices behind your design decisions than being told “trust me, it’ll work”.
Hey! We were not really sure how to pass on the information back when I wrote this in November, but since then we've packaged an opensourced all agents and AI stuff involved in that post: https://github.com/informalsystems/quint-llm-kit
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.