Isn't it more like:

    Verification: code does what the specifications say

    Validation: specifications describe something we wanted to build

This needs a new category:

AI verification: AI meticulously abuses all available loopholes to deliver answer expected by operator, rather than actually responding to the problem.

Simplest example: proof that `x+1 > x` (borderline impossible)

> A good moment to remind everyone: Verification: Code does what it says. Validation: Code does what Specifications say.

Isn't this the exact opposite of what "formal verification" means? First sentence on Wikipedia [1]: "Formal verification is the act of proving or disproving the correctness of a system with respect to a certain formal specification or property."

[1] https://en.wikipedia.org/wiki/Formal_verification

It's still great if the assertions in your code are provably correct.

Every verification needs a spec, and in this case the spec is the Postgres implementation. I think we can and should do a lot better than taking 2.6 million lines of C code as the spec.

In general, the spec must be human readable, and I believe to achieve that we must do away with SQL. Putting aside the thousands of pages of SQL standard, even the core subset has a gnarly semantics due to issues like nulls.

A simpler semantics is one of the main motivations behind Prela [1], and despite its simplicity, we now know it’s powerful enough to express thousands of queries in the wild [2], as well as run doom [3].

[1]: https://prela-lang.org/

[2]: https://github.com/remysucre/prela/tree/sqlstorm

[3]: https://github.com/remysucre/prela/tree/doom/

> I wrote a compiler that can translate both Rust and C code into Lean

How do you verify this compiler is correct? To do that, I think you at least need a formal semantics for both C and Rust in Lean, both sound like Herculean efforts

Have you heard of Aeneas? In case you did, what are your opinions on it? Specifically, why you didn't choose it for your project.

Does your bilingual [Rust|C] -> Lean compiler fork rustc or clang, or other? 12% is promisingly high. I'm still hoping for a world where you can prove critical behavior w static analysis cheaply and practically. The overlap of LLMs and PLT feel under-explored to me

pgrust is incredible btw

Which models do you see to be productive for the task of writing lean? Big fan of pgrust.

So far, I've proven that about 12% of the code behaves the same when executed single-threaded.

Dude, this is a database.

Concurrency is the source of all the hard stuff in databases.

Databases without concurrency are super-trivial.

I don't see any fundamental limitation that would prevent this from scaling up further.

The fact that you've dodged all the hard stuff is a pretty fundamental limitation.

Model: https://github.com/theorem-labs/rocq-linux-process-semantics based on https://github.com/mit-plv/riscv-coq and Sail Binaries are split into sections with a Python script and imported into Rocq with rocq-read-file Workflow: https://theorem.dev/oss-verify/ , https://github.com/theorem-labs/oss-verify , https://github.com/theorem-labs/oss-verify-proofs

Exactly. How do they now that the spec that was generated was correct? Is the spec also AI generated, and could the models lie to make a spec they can verify, just like they lie to make tests pass?

It is also interesting how the LLM optimists are leaning on tools like Rocq and Lean to save them from the mess of uncertainty and confusion. These are tools created by people who understood their code and worked with deeply with type theory etc. People can keep thinking they can get away with making products from vibes, but down in the infrastructure they still have to depend on people thinking and building carefully.

It is hypocritical to campaign for "nobody will look at code anymore" while depending on the hard work of people who carefully look at code.

You could search “decompilation into logic.”

A lot of people think more jobs overall will be created from this. I sort of agree. However, our day to day has changed so much. The problems that I found fulfilling to solve are now handed off to LLMs, but at the same time I can build the things I want to build easier and faster. There are tradeoffs for sure. I'm trying to stay positive though.

I think the answer is: Think of yourself as a maker, not as a programmer, and you'll be good.

I feel like a good chunk of my skills that I honed over decades as a software engineer are obsolete: programming, debugging, navigating code. But there are other skills and especially experiences that, at least with the current level of tools, allow me to do much more than someone who doesn't have them: knowing what computers can and cannot do, or only inefficiently; distributed systems; deployment; CI/CD pipelines.

I feel ya. I've been grappling with the fact how this field has been completely uprooted. On one hand, I see this as another layer of abstraction: I don't know assembly, yet I can command the processor to do stuff via python. LLMs can be seen as another layer of abstraction that allows us to write higher volumes of even more complex software. On the other hand, I can see how programmers can go the route of the chimney sweepers. I try to be optimistic but feel fearful as well.

Hang in there! What you can build knowing how to code is drastically different from what promptards can build. Imagine trying to build a car without knowing anything about car building - you’d just get the most generic boring clunker anyone can design.

Feel you bro, same age, same feelings. And even though AI won't replace me, the work is shit now. I like to code, not to babysit some retarded genius.

> I'm not going to go to the trades

I find it unrealistic anyway, that market will be saturated so fast, it won't make a difference for you or me, in the grand scheme of things.

Automated proofs do sound very neat but I think they'll be constrained to a vanishingly small set of already paranoid domains like cryptography, aerospace, etc. Everywhere else is going to spend the dividends on shipping more unvetted code faster, we're just trading discipline for velocity.

Piss bottles are easily explained by rent though. You get more productive, so the landlord ups the rent, and you have to produce more for the people owning the scarce land (your landlord, the grocery store's landlord, the farmer, etc).

Software doesn't have this scarcity dynamic. People will use LLMs to build better sounder foundations (as rust is 'better' than c) and code quality will improve as we migrate to them. You won't get screwed on your rust++ license though to the point you have to piss in bottles.

Llm adoption has just accelerated people's tendencies. Slop generators generate more slop. They're also finding and fixing bugs that have existed for decades. The societal incentives towards slop we will have to figure out but that's not new - for folks not on that wavelength and for when we get over that impulse at some point it's good if it can also do this. Just in general so sure does write a hell of a lot of tests. If it gets good at it this could pretty easily just become part of the agent loop and we get whatever wins we can from that.

AI is the dark energy of engineering - it pushes us further apart, faster. Some of us get pushed towards slop, others towards formal spec validation, and as time goes it will be harder and harder to see each other.

A while back a knowledgeable man was a philosopher, and they could all easily talk to each other and understand. As time went we split up - we have philosophy doctors in various fields who have very little to talk about.

This happened again when the term “engineer” fractured (even before software engineering). Software engineering itself fractured, too.

And it’s happening again now.

What you're describing is a language that can effectively take a high-level design doc (limited to a formal language representing a pseudo-English-subset) and compile to almost arbitrarily complex, formally verifiable systems. I say systems because you're also implying these could essentially orchestrate distributed systems.

Which, if that were really possible, would be pretty good evidence of AGI. Or, at least, the end of 6-7 figure software engineer salaries. Conversely, I think it's a pipe dream. Writing a compiler that actually works well across such a broad range of hugely complex behaviors would itself be absurdly complex.

Depends really. I tried some experiments towards a pretty uniform relational language for expressing ordinary logic, temporal logic, requirements etc. It does work, but there's some unexpected obstacles.

You'd think performance would be easy to achieve because you'd just write clear, high-level declarative facts and LLM + good optimiser + proof certification system will get you there in terms of performance. But you'll be surprised that relational/declarative specification gives you so much behaviour 'for free' that choosing what to actually compute from those relations is a very deliberate choice. It starts to look like finding an imperative-like path of demand through the relations. It seems that you get exactly the same problems but one level up.

I needed a chuckle and this delivered - “Typescript for SQL” gives me a mental image of a plane crashing into a train wreck.

Yes, that was the vision of 4 GLs and Japan's Fifth Generation Computer project.

However just like the uptake in SaaS, iPaaS, serverless, managed cloud environments, this means way smaller teams will be needed, and everyone that doesn't get to press buttons at the software factory, will need to find another occupation.

> I think somewhat of the opposite will actually occur. LLMs won’t formally verify LLM generated imperative style code.

This result is exactly the opposite. They're verifying at the machine code level, which is totally imperative.

I think this is indeed the direction, but am wondering is anyone actually trying it right now? Love to explore it.

I think for now the answer to adaerlangsql+++ is just Rust - but its semantics have always been about human usability.

Humans have this thing where we can only keep 7 things at once and have to juggle our context, but recall seems much more broad than model contexts.

If we were to start designing a language and toolkit based around LLM context sizes, limitations and quirks - how would that look?

Also terseness and operators are one thing, but what if it’s the other way around - English words etc - can have a much bigger vocabulary of things that can be done but can easily be generated on the fly.

For a new LLM language realistically you would need to probably either write or convert a shit ton of software to it first if you are to train an adequate model on top of it …

And also what about “IDEs” for agents? So far they are clumsily using human tools - just looking Claude string along bash loops and greps to try to eek out meaning form code _it itself had written a week ago_ is frankly frustrating.

There must be a better way and some rich agent specific tooling for code exploration and verification.

Anthropic stance has always been “yeah we tested them all, grep is better” but I still am not convinced - just by the fact that it constantly fails one or two attempts before “figuring it out” yeah it’s fast anyway but it could be _faster_ and could allow the agent to “think” in code space more and not have to validate itself at every minute step …

I think somewhat of the opposite will actually occur. LLMs won’t formally verify LLM generated imperative style code. We (including agentic development) will move on from imperative languages, skipping functional and move to deterministic declarative languages.

I’m generally cautious/sceptical about the current LLM hype, but if that did ever happen and it worked to a useful degree, it might truly be a significant advance. I’m not saying that just because of the LLMs themselves, though.

To reach that point, we would first need to overcome the classic problems in this area:

1. How can you specify the required behaviour for a system in precise detail without ending up with a specification language that is essentially another programming language with similar complexity to the ones we use today?

2. How do you solve the sufficiently smart compiler problem so that producing reasonably efficient and reliable implementations of those declarative specifications is not only viable but expected?

And then, if you still need someone (let’s call them a “developer”) to carefully specify the required behaviour of the system in detail, and you also know how to reliably generate a good implementation of a specification, how much value is left for LLMs to add in this picture?

Maybe LLMs really could be trained to reliably produce good implementations in that scenario? Never say never, but it seems more likely to me that we would develop deterministic algorithms for doing so. That’s already a very hard problem that a lot of smart people have explored, but if a solution could be found, most likely it would be strictly better than relying on LLMs in this part of the process.

Maybe there would still be a role for LLMs to convert natural language problem statements into specifications? Maybe for systems that don’t really matter, that would be enough and a big time saver. However, I’m sceptical about how much time it would be likely to save for systems that did need to work, where you would still need careful design and review of all the detailed specifications by developers anyway.

Maybe LLMs would end up in a similar role to the scaffolding tools that are popular in some ecosystems today, where you feed in some basic choices and the tool then produces a first pass at the files and code you might need, which you take as a starting point for the real work but without wasting so much time on boilerplate? That seems realistic and useful, but it’s a relatively small part of what would then be the overall development process.

In short, I would love for the existence of LLMs/agents to push us towards those better programming languages and tool chains, but if that did ever happen, I wonder how much benefit LLMs/agents could still offer once developers had the more powerful languages and tools available and could work at a “higher level of abstraction” themselves.

Buzzword salad, yummy

I think it won't happen because people just care to much for performance. You already see this now. You see a ton of rewrites moving to rust even from higher level languages.

So Inform7 like languages generating Rust code and then binary code and linked against the OS.

i dont even think that it would be possible to build a declarative language that is flexible enough to do what an imperative language is capable of without being an imperative language itself

> They’ll compile down to be able to run performantly for game development or even for the Linux kernel (as if Linus would ever agree lol) but also they’ll be able to run on distributed execution engines with effectively a shared memory space, etc.

Linus doesn't have to care, MirageOS already exists for OCaml, and I'm pretty sure there's something like MirageOS for Rust...

"leading them to suggest that LLMs will hit a wall in mathematical capability just beyond the convex hull of human mathematics."

This was to be expected, llms are trained on a very large corpus of data, they 'look' like creative from our point of view, as humans don't have that much knowledge, so, if the LLM proposes something that a human does not know, it looks like creative. But they stay neural networks after all, so very good in interpolation, very bad at extrapolation. Building new knowledge is extrapolation if it's truly outside the convex hull how the dataset.

I usually write code and ideas that are at the border of the convex hull, I haven't seen yet an llm being able to propose a really innovative solution. All the time they reuse building blocks that are already there. And I really tried pushing by making them creating proofs.

If I have an insight on some problem and I ask for the proof for it, it will usually be able to generate the proof, but that proof is never creative, and often it will use novel ideas only if I explain the novel idea. It will not come up with it alone. (And sometimes it's very hard to even explain the ideas, as it tends to return to knew waters)

Its only a data point, but I haven't seen a paper that handle this issue yet, and I don't expect them to magically become good at extrapolation due to the theory behind neural networks.

Writing proofs is just writing code in a niche language (that's what the Curry-Howard isomorphism is all about). Writing modular proofs with better abstractions is just writing modular code with better abstractions.

Yeah agents need to step up their programming game in general. They write too verbose code and are happy with duplicating code. This works up until the code is so big that they can't process the code base effectively.

If I had to guess, if you train agents to write better proofs (better modularized, etc), they will get better at programming in general. Or at very least, better at writing Haskell, since so many theorem provers are just sufficiently powerful functional programming languages. And if you get better at writing Haskell, you probably get a little better at writing Rust too. That's why I think this skill probably generalizes a lot.

So maybe training agents to do math will get them, like, use Creusot [0] or flux [1] or Aenas [2] to write proofs on their Rust code, and even when they don't, they will probably write code in ways that are more amenable for reasoning

[0] https://creusot.rs/

[1] https://flux-rs.github.io/

[2] https://lean-lang.org/use-cases/aeneas/

A little before that was:

> The most striking feature of agent proofs is that they are verbose, repeatedly spelling out details about the program’s execution: specifying the contents of CPU registers, explicitly writing out integer conversions, explicitly spelling out that many different addresses are all distinct from one another, writing out the exact contents of stack addresses, explicitly considering every possible branch in a function, etc.

> To be sure, these details are important to precisely reason about the execution of code. However, human proof engineers would have immediately introduced abstractions to factor out these types of repetitive specifications.

- - -

This matches my experience when I look at the tests LLMs write to check their own work when I’ve given them a task. The tests are almost universally terrible because they hard code everything in the most brittle way possible. They are nearly useless for regression tests because if I change anything about the source, even in non material ways, the tests all break in stupid ways that aren’t checking any important properties.

If I have the LLM make the then it also has to rewrite all the tests in a new episode of brittle concrete hyper-literal tests. The concept of a regression suite is non-existent.

It’s probably just as well. Having the implementer write the verification is generally a bad idea with people, maybe the problem of carrying over assumptions and blind spots and misconceptions applies to LLMs as well.

One might say it’s operator error, and I’m underspecifying things, but if I have to go to such elaborate lengths to get it to do what I need, I’ll just implement it myself.

> LLMs will hit a wall in mathematical capability just beyond the convex hull of human mathematics.

I love that “convex hull” analogy. LLMs can certainly serve as a channel for knowledge transfer. They can help spread knowledge and know-how throughout society, enabling breakthroughs that were simply held back by practical limitations (e.g. lack of money, time, or expertise). Personally, I think LLM is more valuable as a tool for democratizing knowledge than as artificial intelligence.

> leading them to suggest that LLMs will hit a wall in mathematical capability just beyond the convex hull of human mathematics

I mean, even just that would prove to be a very productive workhorse - potentially being able to automate away almost every white collar job.

I agree with the observation but not the extrapolation. After all, RLing on sufficiently hard problems might cause agents to adopt better proof strategies emergently.

Sounds like a software problem.

Experience from other agent-based verification projects, such as MachCSL, suggests that the answer might be no: the agents hit a complexity wall with the verbose proof style, and scaling up requires the proofs to be structured around better modular abstractions and reasoning principles.

This is not just plausible but in fact the most likely result.

We already have plenty of evidence of this phenomenon in programming. LLMs are awesome for working on human-written or at least human-reviewed codebases.

But when you set them loose without a human around to force them to refactor their code into something that fits in meatbag-brain-sized contexts, they drift into the ghastly nightmare of the Anthropocene (go ahead, take a look at the leaked source code for Claude Code). They can handle this for a while, especially if you're doubling your model's weight count every four months.

But when you stop doing that, they choke on their own spaghetti.

It's like Feynman said about teaching -- great theoretical physicists need to re-explain the basics to students from time to time in order to force them to come up with not just the correct physical laws, but the simplest version of those laws. Take away that constraint -- IAS or LLM -- and eventually it all goes wrong.

The difference between math and software verification: in math, the convex hull hypothesis implies that you don't go far beyond human capability, because the bottleneck is out of distribution generalization. In software verification, you can verify just about all the software that exists despite the convex hull hypothesis, because the bottleneck is just scale.

From the article:

> Proving that a fuzz test has no more crashes to find is more significant than it sounds. It’s common for fuzz tests in real-world code to test for violations of meaningful high-level properties, such as encode-decode roundtripping, idempotence, algebraic laws, differential testing, self-consistency, or equivalence to reference implementations. For example, a fuzz test for the LZO compression algorithm asserts that if you compress an input, then decompress it, the result is the same as the original. If the property does not hold, the program crashes—so proving the test never crashes is equivalent to proving the property itself.

However, you're correct that this is not formal verification in the sense of a correctness proof against a full specification validated to capture what the program is intended to do. Pretty impressive though.

That's not what they did.

What they did is tried to prove that the conventional fuzzer won't find crashes. Where they found counterexamples, they fixed the bug and tried again.

In essence, a fuzzer takes random samples out of a space of possible inputs that could crash. They proved that nothing in the space of possible inputs could crash.

This is a strictly more powerful result than a fuzzer could give you.

Yes. You are missing something. They are proving that for all possible inputs the program doesn't crash for a given size of potential inputs at the machine code level. The proof extends to an entire set of inputs and all the code it touches, not just the cases the fuzzer covers. In short, they have better coverage than any fuzzer.

Turning buggy software A into buggy software B, with all bells and whistles (and bugs included). This is useful for doing large-scale restructuring of codebases. You can verify you aren’t adding (or removing) bugs.

The main thing they focused on in that is just cybersecurity. Formal verification to try and get rid of surface area for vulnerabilities. Seems like a good idea idk. It also sounds like they're just kinda getting started with it - we'll have to see what opus 5.6 or 5.7 looks like after they've RLed on it a bunch

How do you gain confidence that your theorem actually applies to your code?

I'm curious about your workflow (or the one in the blog post), I have been doing some experiments proving things about existing binaries and it's been extremely slow progress.

it has always been so that being able to read and write code is the first step on the rung. Once you get experience, you start to focus more on higher level concepts of what won't work, what will be annoying to maintain, what will be slow, what will be annoying to extend, and what will be acceptable to the other groups of humans you work with.

I think learning to code will still help with the other things here - its a good first step, even if its now obsolete on a direct level. Like how its useful for mathematicians to be able to calculate by hand even though calculators exist - it gives intuition for how to operate the tools and check results

This doesn't follow. We've had code as trusted as that for _decades_. Common criteria and EAL was certified at the end of the 20th century. Before that there was the rainbow series in the US dating back to the 1980s [1].

It's absolutely cool to see this sort of validation process get cheaper and easier, but it means nothing if no one cares enough to do it. EAL1 certification can be as cheap as a beefy server, but it's not commonly done because effectively no one cares.

As microsoft learned with the zune just because it's cheaper or better at the same price doesn't mean anyone will use it. Culturally, we have to make the effort of verifying code worth it.

[1]: https://en.wikipedia.org/wiki/Rainbow_Series

Code needs to run on physical devices, which are prone to undervolting, bit flips, hardware bugs in specific batches, radiation, deterioration, and the like.

Preferably, I wouldn’t trust my life to a calculating device running on AA batteries while dangling from a rope.

I think it's a really illustrative example of how to play to AI's strengths. No human would dream of writing 600,000 lines of Rocq to verify one binary. The whole approach is so insane that it probably wouldn't even occur to them. But Claude has no concept of tedium, and will happily fill out lemmas all day long until the job is done. To me that's what's significant about this result: it's not about scaling up an existing technique, it's about using scale itself as the basis of a new technique.

I believe that they chose assembly in order to diff against real projects and then see if those real projects have bugs.

How do you know any test is checking what you want? You either review it, and/or you run the test on things you know are good and also things you know are bad.

If you have a model of the programming language, then you can make proofs about the source code itself. At this point, your assumption is that you are accuratly modelling the compiler.

You can go a step farther and model the instruction set and architecture, and which point you can make proofs about the final binary directly (thereby sidestepping the problem of compiler bugs). At this point, your assumption is just that your physical hardware actually matches your model.

> Couldn’t it very well be that you proved something that wasn't actually your program?

Correct. It can happen, where the actual code, could diverge from a lean representation of it, in a glaring or subtle way.

> how can you be truly sure that, when formally verifying a program, you have correctly modelled the software you’re trying to verify?

You can do it backwards. You declare the properties you want the resulting program/function to have, using a proof assistant like Lean, then prove that a program exists that meets those requirements, and the proof assistant spits two things: a confirmation that the proof is valid, and a piece of code that implements the proof, in the form of computer code.

At least that's how the proof assistant Coq would often be used. You still have the challenge of ensuring that you have defined the properties you really want in the first place, but at least it solves the part where you want the code to meet the specification.

I mean ... The thing about formal verification is that you can write the extremely slow but correct version of your code and then have an optimizer write a much more efficient version with a proof of correctness.

For things like programming languages we often have tedious, but slow, semantics that can be directly implemented in a suitable language. Then really all that a compiler or interpreter is is a faster version of those semantics.

If you are able to show correspondence between the fast and the the correct version, then you can toss the correct and slow version without even ever running it and just defer to the provably correct fast version.

Most software is ultimately like this

What a tiny subset of all TLA+ articles (a very popular topic on HN)...

2017: Leslie Lamport: Video course on TLA+ (328 points, 74 comments) https://news.ycombinator.com/item?id=13918648 (219 points, 2018, 17 comments) https://news.ycombinator.com/item?id=16956778

2017: Writing correct lock-free and distributed stateful systems in Rust, with TLA+ (374 points, 94 comments) https://news.ycombinator.com/item?id=14373359

2019: TLA+ model checking made symbolic (197 points, 51 comments) https://news.ycombinator.com/item?id=21662484

2019: Introduction to TLA+ Model Checking in the Command Line (176 points, 44 comments) https://news.ycombinator.com/item?id=18937214

2019: Learn TLA+ (387 points, 92 comments) https://news.ycombinator.com/item?id=19661329 (310 points, 2020, 58 comments) https://news.ycombinator.com/item?id=22393653 (254 points, 2022, 64 comments) https://news.ycombinator.com/item?id=33010645 (350 points, 2022, 75 comments) https://news.ycombinator.com/item?id=31952643

2020: Using TLA+ in the Real World to Understand a Glibc Bug (166 points, 76 comments) https://news.ycombinator.com/item?id=24958504

2026: Hunting a 16-year-old SQLite WAL bug with TLA+ (239 points, 29 comments) https://news.ycombinator.com/item?id=48730953

...

https://hn.algolia.com/?dateRange=all&page=0&prefix=true&que...

I don't get what you mean? Granted, I didn't even try reading your message, since the language that you're using, English, is not sound, complete, decidable (or even defined).

_these_ programs not _all_ programs

what is sharpee. chord ?

no idea what you are even talking about

It seems like it’s a good fit. Proving equivalence is much easier than writing a spec without a golden reference.

Except COBOL systems are often easier to formally verify than modern systems.

They're often simpler, and whole classes of security vulnerabilities are mitigated by design. My favorite example is SQL injection mitigated by having proper access controls in the DB. Why prove about every SQL statement that it cannot be nefarious, when we can just prove it about the connecting user? The user access carries the intent of what the application program wants to do with the database, in a separate channel, independently of the complexity of the application.

I think you still run the risk of common-mode failure. It might be more robust to pick a different model altogether to do either the VM or the spec.

ESBMC: https://esbmc.github.io/

It's why unit tests are worthless when humans write them, and less than worthless when AI writes them. Same concept: you're testing yourself, of course you're going to pass with flying colors.

If you want it to do that consistently why can't you put it in your Claude.md?

Nohow, because the real world is informal. This is as far as coding can and will ever go, basically.

And like yes, it does just launder defects to a layer higher, but another way to phrase that in this case (and in many other cases) is that it raises the bar.

Instead of defects being mostly about nonsense minutia (relative to business logic), they are about actual design decisions and their correspondence to reality, i.e. the actual original goal and point of this god forsaken, navel-gazing field.

You do it by comparing to something that is “known” to be good.

I didn’t read the whole article, just the appendix. There they talked about having Claude write a python interpreter. Then they had it write a set of properties to test and they vetted the properties against accepted existing python interpreters.

Proving two things are equivalent is a major component of formal.

For everything else, formal is only as good as the properties you specify. A long standing problem. But it’s a problem for all verification. If you write a shitty tests, you get shitty verification.

A key difference I think is that the same skills used for evaluating and reviewing application code apply to reviewing test code. That’s not really true for formal.

Hmm? I had Claude Opus 4.6 implement a .NET compiled language that is Python-like (we already have IronPython, I wanted something Python-like that treated .NET as its entire runtime) language in about two (maybe three sessions tops?) of 1M token context windows, and the first two times I only used roughly 400 to 600k tokens? When Anthropic dropped the 1M context window update, I put it to the test.

See for yourself:

https://github.com/Giancarlos/Culebral

Anyway, my custom (currently paused because I'm taking on a much more ambitious compiler project with Claude... just to push the limits) language can build ASP .NET applications, and a bunch other things. I also took the Rust approach to types, all method signatures must have types defined, type hints are inferred when declaring new values from the value on the right.

I've also had Claude rewrite legacy C# projects with 100k+ lines of code, fully in Rust, long before Opus 5.0. I've spent the last year pushing the limits with Claude, including reimplementing existing software, which people are catching on to now, and I've managed to get rather far in some cases.

So I wouldn't be surprised if yes, Claude can implement Python, mind you, there's Python interpreter coded in Python in what was it? 500 lines of Python? You can build a Python stack machine bytecode interpreter in like 60 ~ 80 lines of Python code.

Would not surprise me if you can trim a C programming language interpreter down in terms of lines of code when you rewrite it in Rust especially when you have access to a much more functional language, not to mention Rust took the best bits out of OCaml it could to make itself very efficient at writing compilers / languages (so they could write their own compiler in Rust...).

I am also having Claude building me a much smaller compiler, which started out in under 500 lines of Python, but as I got more ambitious it had to write more code for my language, it was meant to be a slightly less restrictive Go, the Python basically converts the syntax to C which then compiles anywhere. Havent put that one on GitHub since I'm still tinkering with it.

The halting problem applies when you are trying to check the properties of arbitrary programs. However, we are not writing arbitrary programs, we are writing very specific (hopefully useful) programs. The two are very different.

Pop-sci explanations of the halting problem have probably done incredible damage to formal verification as a whole. Mostly because it makes people with only the most cursory understanding of it go "why bother, it won't work anyway."