- 94comments
- —discuss
- 150comments
- 39comments
- 14comments
- 58comments
- 1comments
- 70comments
- 352comments
- —discuss
- 30comments
- 50comments
- 141comments
- 157comments
- 630comments
- 254comments
- 97comments
- 5comments
- 174comments
- 80comments
- 10comments
- 239comments
- 53comments
- 150comments
- 165comments
- —discuss
- 22comments
- 74comments
- 28comments
- 30comments
Some noteworthy lines from the README.md[0]:
[0]. https://github.com/bendlang/bend/tree/main
So are Haskell's, since 20 years ago, with no options for years?
We will introducing binary buffers eventually. The project is new...
“No options” simply isn’t true. Here’s a guide to many of the options: https://hasufell.github.io/posts/2024-05-07-ultimate-string-...
Now if you’re asking why the basic prelude String type remains as it is, that’s because changing it would break more code than it’s worth, at least as far as prelude’s maintainers are concerned. This is no different from how standard C strings remain a null-terminated sequence of bytes even though that’s been awful for everyday use for at least 30 years.
It seems like this is largely a matter of what you’re asking for. If you wanted to do more research into the state of the field, an AI might be pretty good at answering your questions.
Yes, telling it that you want parsimonious solutions that reuse existing libraries makes a big difference. Why would it even try to do that sort of stuff if you didn’t ask?
Because it should be smart. I mean, why would a human coder ever observe standard best practices unless the client specifically asks them to?
But it won't tell you if you don't ask. It won't tell you, "This approach is stupid, Ada SPARK exists".
Why would any LLM 'think' in terms of trying to cite prior work?
It itself is prior work. It's asking a fish to show where the water is. The fish can't imagine that absence, and the LLM can't imagine anything not being prior work.
Nowadays AI chat often will do web searches and include links. It will do that more if you ask.
The original discussion about the project (https://news.ycombinator.com/item?id=49746163) is very weird. Lots of call-outs about how the author is some sort of celebrity and random accounts vouching for him, with little discussion on the substance.
Not even the demo on that release works well.
The whole original conversation was very smelly from the very start, 20k stars included on the GitHub page with lost history.
Does anyone know where they bought the popularity and contributors from? I would like to do this for my joke language to fool unsuspecting users into using it seriously
Yeah 100% those are purchased/fake
Lean4 itself has 9k
The Bend1 launch was very successful, with 1000+ hn upvotes [0] and with several youtube videos with up to 1M+ views [1] [2] - that's where a lot of the popularity came from, I believe. They just recycled the Bend1 repo for Bend2 even though it's a completely different language.
[0] https://news.ycombinator.com/item?id=40390287
[1] https://www.youtube.com/watch?v=HCOQmKTFzYY
[2] https://www.youtube.com/watch?v=NaytZOiX3fs
The history is back...
We know what kind of turf that is.
I posted a sharp critique in the original discussion, aiming to be civil while critiquing the project. I may have been a bit terse, and would probably rephrase some of it now to avoid confusion, but I don't think I was ever outwardly disrespectful.
I received several very emotionally charged responses centered in the personal credentials of the author. They felt very out of place and did not engage substantively with any of the things I said. It was indeed very weird
The author, who I hadn't heard of before yesterday, actually seems like a cool dude. He was quite responsive, normal, and engaged with my feedback, which makes other random accounts being offended on his behalf all the more uncanny
I think people responded that way because you strongly implied he was an unserious vibecoder who was just fooling around, and you called him suspicious as fuck.
Your post and the ones that followed are a good example of the contrarian dynamic that dang often talks about. https://hn.algolia.com/?dateRange=all&page=0&prefix=true&que...
OOTL, could you give a link to a relevant @dang post?
https://news.ycombinator.com/item?id=25140587
I don’t see anything from your parent commenter on the other thread that deserves that classification. On the contrary, while they initially had suspicious of vibe coding, on later comments they are cordial and even admit their own misunderstanding.
What am I missing? Where does “called him suspicious as fuck” come from?
It literally said 'sus af'.
"you [...] sound sus af" at the end of the comment. sus means suspicious and af stands for as fuck.
It was a fair critique, but if you're looking for feedback I think people were probably responding to your last line.
"I'm glad you're having fun vibecoding" comes across as very backhanded and condescending. It sounds like you may have actually meant that genuinely, but it doesn't read that way in text form.
"you sound sus af" is not respectful or constructive in my opinion. It's a description of your own feelings, not a critique of the project, and there's not really any way for the author to respond besides ignoring it or saying "sorry you feel that way" or something.
I think that line undermines the rest of your comment, because I'm left thinking that you don't really expect good answers to your questions and you just think the whole thing is dumb.
Approach itself looked impractical to me for any non-trivial system, like domain centric system of records systems which can have 100s if not 1000s of laws. Though it can be tried as a side parallel thread to see if system is still compliant and following right first principals after a few years from its inception.
I would rather wait to see how it gets adopted, if at all. Anyone aware of early reviews of the adopters of bend 2?
What about it isn't working for you?
Yes I think fundamentally the effort required to understand, write, and verify a formal specification is just way higher than is reasonable in most situations.
There are some cases where it is pleasingly simple - usually low level algorithms like compression, sorting, search etc. Basically things you'd find in leetcode questions.
Most software isn't like that.
I think the actual answer is just that the very latest models (e.g. Astra) are actually quite good at writing normal tests, and you can just skim them to make sure they're doing something sane.
Narrowly, I think you're spot on. The effort required to understand the machinery around formal verification is a function of the surface area of the thing being formally verified. Specifically, formally verifying the surface area of general purpose programming languages is difficult.
My approach with Hale (shameless self plug) is that the programming language itself first offers another strata of structure to program within, a type of graph. Once the structure of the program is expressed as a graph, understanding how formal verification works is a clean encapsulation of graph activities.
If you have to write LAWS.bend which is pure code describing the laws then it isn't basically like those old days of writing unit tests and that too tests first hence the TDD?
So what is the unique idea here except a vibe coded compiler that generates C and everything else is handled by clang+llvm?
From README.md:
Also, why the compiler is not written against and with LAWS.md so that no audit is required at all?
"Know what to ask for" is what will keep me with a job for a while longer, I guess.
The code itself is the most compact representation of the rules you want applied.
This is probably not necessarily true. “f: list[1 A] -> list[A] pure, worst-case time n log n, such that for all x and 0 <= i <= j < len(x), f(x)[i] <= f(x)[j]” is probably good enough for nearly everyone unless the program synthesiser is actively adversarial; probably 99.999% of the list-sorting in the world is done via standard library functions anyway, which suggests that people don’t much care exactly how it happens.
Good point. I would treat this as 'fully specified vs partially specified'. For a fully specified system, my mental model still maintains that the code is the most compact ruleset.
I agree that "don't care" is often the practical choice which corresponds to partially specified. In your sort example, both heap sort and merge sort satisfy the requirement. But they are not always interchangeable because each has a specific properties that you might care about (constant memory vs nLog(n) memory, easily parallelizable vs hard to parallelize and so on).
Not good enough: `f(x) = []` or `f(x) = (if len(x) == 0 then [] else [x[0], x[0]]` are implementations that fulfill your specification and yet they don't always sort the input list correctly...
It will if you remember to ask it. I've got into the habit of starting any new project with a session where I ask a search-enabled LLM to help me figure out what the prior art for a problem is. It's saved me quite a bit of time.
Think you could argue that’s more LLM-assisted engineering than it is vibe coding.
It seems implicit in the article that the author should have remembered to ask, as part of the prior research.
Isn't the usual argument that all AIs can do is build on prior art? Like, I spend a disproportionate amount of time trying to convince my agents that I don't want to just reimplement the Rust borrow checker for my language!
I really wish there were search harnesses, actually. My LLMs are lazy as hell and seem to want to just report the first thing they find on google. I know they can return truly niche and useful results, but it takes a lot more prompting to get them there than I would like.
I've been using GPT-6 Pro in ChatGPT (and its predecessor GPT-5.6 Pro) and it's been incredibly effective. I don't think it's available on anything less than the OpenAI $100/month plan though.
you know that most big ai companies not only have search harnesses but also sota models that are post trained for web search specifically.this is what the deepsearch option is in most cases. and they have been unbelievably good for years now.
The recent OpenAI wiki spam indecent was interesting because it helped reveal some of how they are training their models for research tasks: https://collusion.wiki/
See also this piece on misalignment from OpenAI https://alignment.openai.com/misalignment-reports/self-gener... which reveals one of their RL tasks:
This is just another facet of the sycophancy issue. They really need to start RLing these models to gently push back the way a friend would on things that are questionable.
It would also make sense for them to just RL in the "research prior art" arc as part of that "is the request sensible" pre-analysis. It wouldn't be difficult and it would save everyone a lot of pain.
Yeah, for this to feel credible you need to make sure the model doesn't figure out that you're planning to build a solution yourself.
@LiamPowell the author is clearly aware of formal verification, they've written several implementations of dependently typed languages, and ... despite the presentation of their work, which has some obvious flaws (as can be judged by reception) ... their many comments indicate that they know what they are talking about.
Your post is setting up a strawman between automatic formal verification and formal verification using interactive theorem provers ... obviously there is a spectrum, and Ada/SPARK are navigating the space to try and automate much of the work required to automatically dispatch with obligations to prove (computable) properties about programs.
Bend2 is a QTT -- it's dependently typed, and comes from the lineage of systems which are focused on being expressive enough to formalize mathematics.
Of course you need to build a somewhat significant "standard library" of theorems, tactics (as metaprograms), etc ... to approach what is built into the compiler in Ada. These are different approaches with different trade offs.
Your post isn't clear, you don't go into any of these details ... why did you post this? Do you think this is clear writing?
I'm not familiar with the author, I just saw the language posted the other day. I'll add a note to the top.
Why would we want the tradeoff where the LLM has to write significantly more code and where the specification needs to be more complicated? If the author is aware of the state of the art then I think they made a poor choice, but that's not the point.
Bend just serves as a useful example, my general point is about how people will vibe-code a solution without an understanding of the field, leading to worse results than if they spent a little while understanding the field and then vibe-coded their thing.
If you're going to insinuate that the author of Bend2 doesn't understand PLs and formal verification, you should do so with some proof and not a hot take dunk.
I think it's fine to critique the language and the approach without criticizing the author and I hate that this site has become Tech Drama News, like the worst parts of Twitter.
Yes, I didn't realise how much it comes off as a critique of the author personally when I wrote it. I have added a note to that effect to the top of the article.
conversations on this site about formal methods are currently absolute cess pits of dunning kruger and confidently stated yet highly misinformed takes from those with close to little experience in the field.
I think sadly all big conversations on this site are like this these days. It didn't used to be like that sadly. Z3 and some early Lean threads used to be great.
Perhaps because their concerns are different? Similar reasoning: "why invest in dependently typed languages over SMT solvers? SMT solvers are automatic, and it is way easier to add annotations to my programs"
The answer is that these technologies are not universal in trade off space.
Of course, if you can have an LLM prove something by dispatch to an SMT solver ... you want to do that (and, indeed, LLMs do sometimes do this even when working on Lean proofs)
But the space of statements that you can prove using verification with SMT is smaller than dependently typed systems.
Also, Ada/SPARK are very good and robust -- they've been around for ~50 years ... but there's been a significant amount of work in formal verification since then, right? I would be more clear that Ada/SPARK are state-of-the-art for "mission critical software" (and have been for many years), but there's been a lot of research work in formal verification of low level programming since then (Low*, for instance)
I'm assuming you have not spent a lot of time trying to prove stuff about non trivial programs if the trade offs between SMT based approaches and interactive theorem provers are not clear to you.
SMT solvers are highly automated, but very opaque and hard to debug. Interactive theorem provers can scale to larger problems and harder properties at the cost of increased manual proof burden. The ever increasing ability of llms to write proofs in a theorem prover has in recent years tipped the balance significantly towards preferring itp based approaches over pure SMT ones. The current state of the art for program verification is probably a mix of llm and traditional (tactics, SMT, etc.) proof automation inside an itp.
ATPs go quite a bit beyond what a SMT can do, however you're not stuck with just using ATPs when they are supported. You can still allow for proofs to be manually written with an ATP doesn't work, and in fact SARK allows for this with Rocq.
Most of what I have to prove is floating-point code where a manual proof is too much of a headache to ever attempt though.
---
That's why all your LLM requests to build something substantial should start with "run prior work research first". Of course, at some point everything converges (if we share our outputs open-source) and then we may have solid standard patterns and libraries and do not need to waste trillions of tokens globally to rebuild the same minor, fundamental things, each one in their silent little silo.
IF we share, it will be of course to the monetary detriment of LLM providers who will have less income overall, and of course now they can't repackage anymore all our collective input, thoughts, human 'thinking traces' that they collect in their meta-data, as their new 'innovations' any more to inflate IPOs / stock prices.
Or maybe it should be a flag to indicate that there might be more to think about before handing the task of to an LLM.
As effective as “make no mistakes.”
It is trying to please you, and it always determines that the way to please you is to fulfill the original, core request. Any caveats or first steps will always be secondary to the ultimate goal of “this person wants to do X, so I will do X.”
The only first step I have found somewhat consistently useful, because as we know LLMs do not behave consistently, is when doing tech troubleshooting I will go “look at documentation for X before answering” so that it will search manuals and such. Helps avoid speculation. But even then, it’s still not full proof.
Sidebar: this is one of the core problems of LLM’s currently. You are basically arguing with them to get them to behave a certain way all the time and it’s not always clear if they’re doing what they’re being told to do. Then add the compounding layer that the longer the conversation goes on, the more likely it is to misunderstand or just ignore things as it descends into context-length-induced madness
Those aren't comparable instructions. Providing useful, related context to improve outcomes is a basic best practice, and asking LLMs to do research first is an important source of that.
Humans dont let LLMs raw dog internet web searches.
Yes, but I think there are incentives to not do this for many LLM providers. Doing prior-work research is slow (web searches aren't fast, LLMs are rate-limited or blocked from plenty of pages, etc.), and sometimes contradictory which annoys LLM users, many of whom like faster gratification cycles from the agent slot machine handle.
Also, writing a bunch of bespoke code instead of leveraging prior art makes a lot of users feel like they own something novel/big/important, and also poses a larger maintenance surface for the LLM to make future changes (which costs tokens).
I don't think there's, like, a conspiracy at LLM providers to set up system prompts/RAG/etc. to discourage research-and-use-prior-art-by-default approaches. Rather, OpenAI/Anthropic/Google/etc. are optimizing for real but sometimes misleading success metrics which often lead away from a research-first approach.
Although, I have known using an LLM to do your prior research to itself be a trap.
The searches it runs, and the summaries it provides, are all incredibly sensitive to your choice of words. Words you chose from a state of minimal knowledge. So it’s like a particularly perverse version of the anchoring bias: information that could have led you to a better solution is often actively filtered out of the agent’s response precisely because it leads down a different path from your first idea.
In short, if you ask an agent what’s the best hammer for driving screws, it’s liable not to mention that screwdrivers exist.
Yes this is precisely why experts drive LLMs so much better than novices. It’s also why I don’t dismiss pure LLM output as slop and uninteresting; even if we both are using the same LLM, I probably can’t make it output what you can make it output.
Beautifully written. Hammers for driving screws + sycophancy are horrible together.
- That should nowadays be very obvious. You start any substantial work by doing research. LLMs are [perhaps surprisingly to some] good at that. They are also pretty good at doing the plumbing. That is a godsent in the hands of a good researcher and architect. And I don't have any qualms if tokens are "wasted" on research or on the precursor work. That doesn't replace reading good books on a subject but it DOES replace finding and filling knowledge gaps.
- But that shouldn't be confused with getting the LLMs to make the decisions. I believe that would quickly ruin a good design, unless the decisions are about truly inconsequential aspects, which are very rare in language and API design.
- I don't believe that (sharing) is to the detriment of LLM providers either. Not realistically. We would build faster and the questions / research directed at LLMs would be more sophisticated. Believe it or not, they can't cache questions as easily as websearch queries. If anything, I believe the more people learn to use LLMs effectively (rather than just to generate slop), the more their usage will be ingrained in daily life. Some of that will be redirected towards current LLM providers. But perhaps more of the economic share will increasingly go to hardware providers, as more and more people will be interested to run their own models.
Pro: it can be an excellent way to learn if you realize good problems don't come easy, many such cases where I abandon something having learned from it and that's life
Con: the machine will tell you you have easily found a good problem, and engineered the perfect and necessary solution, if you let it
I haven't seen a language launch this controversial on HN since V-lang in 2019.
Glad we finally have some new drama to follow, definitely more entertaining than AI news.
It's definitely AI related, though.
I think they know the standards of formal verification. They just surf the AI hype, whip up a verbose Python-like language that is worse than any existing prover language and have 20k bots star it.
This is the way to succeed these days.
I checked the developer's X account, they have written numerous posts about formal verification, so this specific claim ("without realising that said field exists") seems to be false.
Back in 2018 they were working on Formality, an Ethereum formal verification project. They are the Victor in this video about it: https://slideslive.com/38911748/introducing-formality
Here's the GitHub repo for that, which demonstrates familiarity with formal proofs that long predates LLMs https://github.com/VictorTaelin/Formality
I don't want to change that sentence now that people have discussed it, but I have added a note to the top to make it clear that I'm just taking it as an example of a vibe-coded program because it's recent and high profile.
My critiques of the language itself are not the main point, although I do still think that it's a very bad design to have a LLM waste tokens on a proof that could be written by CVC etc..
But this is grossly intellectually dishonest. You know very well how this will be read and responded to here ... and you keep saying that you're just talking about vibe-coding oh but you have serious criticisms of the specific effort. You write passive-aggressive stuff like
which contradicts your base assertion that their decisions were not informed. And
You claim
but that is severely factually wrong, which along with a lot else suggests that you have very bad judgment. As the author writes,
IOW, you have made a serious error in logic.
You trashed the author and his work without bothering to learn anything about either one first (which is quite ironic).
I won't respond further.
Bend's developer has posted a well-argued response here: https://news.ycombinator.com/item?id=49753898
I am glad I saw it, as now I am interested in learning more about Bend.
I feel like this is the same black hole as small local models.
Things people want to be awesome and true, and things that are actually awesome and true don't intersect the way people want them to.
…so if there was an easy way to do provably correct AI code, it would be nice.
…but I’d also like a frontier that runs on my raspberry pi and a cheap fully autonomous self driving car that just uses a single cell phone camera.
Unfortunately wanting those doesn't make them exist; and people telling you they do exist usually are either a) uninformed, or b) selling something.
I haven't looked into Bend 2 in detail, but it seems a bit harsh to call it "horribly broken or decades behind the current state of the art". Clearly there is a problem with formal verification languages and there is a demand for something else in that area, and the problem is the usability and syntax. I don't want to have to learn something that looks like Haskell, or to have to wrap my head around Curry-Howard correspondence. I don't want to write my conditions in something that looks and feels like C++ template metaprogramming. I recall a Hello World in something like Coq a few years ago which basically started with "first, we construct the Peano integers", and then they used this to prove that some calculation was bounded - because it seems they couldn't represent integers natively?
I just want to be able to write C#, JavaScript or whatever, and then tack on preconditions, checks and so on with the same syntax. Dependent typing and design by contract for the masses.
This is just about vibe-coded programs in general when the approach assumed by the article is taken. For all I know they did make an informed decision regarding the tradeoffs (which I would consider to be a poor decision).
That's more or less what SPARK (and others) do, although specifications for large programs can become nasty.
It sounds like the crux of the issue here is that you don’t want formal verification in the first place. Your last paragraph sounds more like code contracts, which is also a thing that already exists.
Well, yeah, you have code contracts in Ada or Spec#, (very limited) fixed type ranges in Pascal, ... but no general purpose programming language lets you put an arbitrary expression in the same language in a type as a permanent condition, or lets you state facts that the compiler will prove.
Of course not, that would be equivalent to solving the halting problem, many people will say.
I wonder if that will change now: I'm happy with an imperfect sanitizer that I run every now and then and will run a couple of minutes and come back with: I've proved your conditions, I proved a violation, or I can't decide, please change your code.
Lean can be used as a regular programming language. There's also languages like idris2 and f-star, but they don't seem to have much traction.
Finally a bit of sense in this madness.
The obvious botted stars on GitHub in 2 hours was an immediate red flag.
A language for LLMs will never be a compiled language. The best language for LLMs would be something that can be interacted with. Like a Lisp.
I wouldn't use SPARK either, and rather develop my own approach. The problem isn't that the proof has 400 lines of code, every modern system has large proofs (Isabelle/HOL, Lean, etc.) My latest formal proof has over 50K lines of proof. That's why AI is such a useful tool.
A vibe-coded retort to a vibe-coding tool? Ugh.
"The developer has built an entire language around a field seemingly without realising that said field exists."
That is incredibly funny.
Here's a talk about formal verification I made 7 years ago @ DevCon:
https://www.youtube.com/watch?v=0fg1QbeeqNU
Here's Cedille Core, my implementation of Aaron Stump's self types, a Computer Science professor who taught me a lot, ~8 years ago:
https://github.com/VictorTaelin/Cedille-Core
I also implemented Kind-Lang 5 years ago, way before LLMs:
https://github.com/higherorderco/kind
I dropped out of Federal University of Rio de Janeiro to study this subject independently, because I was passionate about it, and I spent nearly 10 years doing so, daily, on weekends. That's what I do.
Bend proofs being verbose has nothing to do with me not knowing that inference, unification, or program search exists. Kind had these, 5 years ago. In fact, I've also been researching the later, and I built SupGen, which overperforms every published symbolic program synthesizer in the literature by 10x or so. This is unpublished yet, but you can find my posts about it 2 years ago on X (I'm @VictorTaelin).
So, why is Bend verbose???
Because it makes it fast. It is intentional. It is my vision that a good proof language should be fully explicit, because this reduces proof-checking time significantly. That is what makes Bend realistically 10x-100x faster than every alternative.
But wouldn't that mean it is much harder to write it?
No. As you said it yourself, we have tools that can fill these proofs today! Not just AI models. You can apply these tools to produce Bend proofs, while the language itself remains a thin, dumb proof kernel that does one thing, and does it well.
If nobody is reading these proofs (because they're written by AI and automated tools), then, it is, in my opinion, irrelevant, as proofs will eventually become a layer nobody looks at, just like generated assembly.
Of course, I could be wrong here!
But it is misleading, if not just a bit malicious, to claim I "vibe-coded" a language without knowing about a field I've spent a decade researching about.
Every single part of Bend is an intentional choice I made after considering every alternative. I use LLMs to fill code after I make all hard architectural decisions because they type faster than me, and I'd rather spend my time doing useful experiments than typing trivial functions, even though I could.
Incidentally, deciding what I should NOT include took me way more time effort than any line that was shipped, and there are perhaps millions of lines of code, manually written by me, that I threw away, backing up these 4k that went into the final design. An artist once told me you must first paint a Rembrandt before you can draw a cartoon that's simple in the right way, yet that might mislead someone who has never drawn into thinking you don't know what you're doing. I guess.
Sorry. See the edit at the top if you haven't already. I didn't realise how much it came off as a critique of you rather than a particular approach to software engineering.
---
I disagree with LLMs manually writing proofs without other tools doing all the work they possibly can ever being a good solution for a couple of reasons:
1. Tokens are really expensive when we have a LLM spending hours hacking aware at a proof, not to mention generating those tokens is slow.
2. The context window becomes flooded with proof work rather than work on the original problem, which will lead to a worse solution. LLMs are demonstrably worse at writing code when you continue a session on a new task instead of starting a new one.
We can cache the results and help the checker along with assertions rather than throwing out all the smart parts of the checker.
I was really confused when reading the article that their claim is you don't know formal verification, I was expecting something way juicer.
"This example matters beyond Bend, vibe-coding makes it makes it far too easy to implement a design that’s horribly broken or decades behind the current state of the art because you can immediately get a result without ever having to do any research."
This is totally true but almost totally irrelevant. I'll use some hyperbole here to make the point: Whether the design is broken or decades behind doesn't matter anymore. Neither of those are an outcome/end goal. They are means we historically have used to achieve good end goals or outcomes.
In the end, the goal is usually "does it meet the needs of the person who needed it" not "is it good software". If it no longer meets their needs and they can vibe code another total piece of shit in an hour that meets their needs again, they still may be "better off" than spending time researching the field and learning and ...
This may feel shitty, and it may feel like it should not be true. But right now, that seems to be true?
In that sense, the author is wrong that vibe-coding is a trap. The trap is assuming you have to make something good to meet someone's needs both now, and in the future.
Now, like i said, this is hyperbole, and there are lots of good arguments against it. The author's just isn't one.
Technically good or better has never mattered very much in the marketplace, despite people wanting it to really badly (ease of use often mattered, but not technical goodness). Software engineers often took pride in their work and so there were usually kernels of goodness in even the shittiest software. All you are seeing is that now it is nowhere near as hard to create and bring these "solutions" to market, and more importantly, doesn't necessarily require anyone who has any pride in their work at all, or even have any experience in software engineering. As such, technical goodness has mostly gone out the window because the market never required or really rewarded it.
I find this to be a mean and misguided post. To suggest that Victor Taelin does not know about formal methods. As I understand, he is trying to do something genuinely new and interesting. And he is transparent about his work, which he then gets hounded for. A shame.
Why is it mean? The author is above critique?
I found the post offputting because he is insinuating a few things about the author which are clearly untrue (eg, unfamiliar with the formal verification landscape) and he's using this untrue speculation as evidence of the dangers of vibe coding. Even the edit where he says swap it out with a hypothetical person who fits the description - it's still leaving in the untrue claims about the author.
God forbid someone criticise Victor Taelin!
This is precious.
Very off-topic, but the 'humans write “laws”' phrasing made me think of using LLMs to unit test real laws. Have them come up with test cases to see if the phrasing is as intended or has loopholes. Wonder if anyone's tried doing something like this (probably not, I imagine this is too much tech for government)