Live data from Hacker News

Leanstral: Open-source agent for trustworthy coding and formal proof engineering

mistral.ai

151–160 of 234 posts

Re: Leanstral: Open-source agent for trustworthy coding and formal proof engineering

#151

It’s great to see this pattern of people realising that agents can specify the desired behavior then write code to conform to the specs. TDD, verification, whatever your tool; verification suites of all sorts accrue over time into a very detailed repository of documentation of how things are supposed to work that, being executable, puts zero tokens in the context when the code is correct. It’s more powerful than ream…

[dead]

Re: Leanstral: Open-source agent for trustworthy coding and formal proof engineering

#152

Curious if anyone else had the same reaction as me This model is specifically trained on this task and significantly[1] underperforms opus. Opus costs about 6x more. Which seems... totally worth it based on the task at hand. [1]: based on the total spread of tested models

[deleted]

Re: Leanstral: Open-source agent for trustworthy coding and formal proof engineering

#153

Earlier quoted context omitted.

Kiro is such garbage though

If you add why you think so we might learn something.

The same prompt in the same project gives different results/slightly worse results compared to Claude Code, both using Opus model.

Re: Leanstral: Open-source agent for trustworthy coding and formal proof engineering

#156
post #90
post #48

Earlier quoted context omitted.

This would be unfortunately a rather nuclear option due to the continent’s insane reliance on technology that breaks its unenforced laws.

How about not making these unenforced laws in the first place so that European companies could actually have a chance at competing? We're going to suffer the externalities of AI either way, but at least there would be a chance that a European company could be relevant. The AI Act absolutely befuddled me. How could you release relatively strict regulation for a technology that isn't really being used yet and is in the…

Because the AI act was mostly written to address issues with ML products and services. It was mostly done before ChatGPT happened, so all the foundation model stuff got shoehorned in.

Speaking as someone who's been doing stats and ML for a while now, the AI act is pretty good. The compliance burden falls mostly on the companies big enough to handle it.

The foundation model parts are stupid though.

Re: Leanstral: Open-source agent for trustworthy coding and formal proof engineering

#157

Earlier quoted context omitted.

The scientific approach is not only or primarily empiricism. We didn't test our way to understanding. The scientific approach starts with a theory that does it's best to explain some phenomenon. Then the theory is criticized by experts. Finally, if it seems to be a promising theory tests are constructed. The tests can help verify the theory but it is the theory that provides the explanation which is the important par…

> The scientific approach starts with a theory that does it's best to explain some phenomenon At the risk of stretching the analogy, the LLM's internal representation is that theory: gradient-descent has tried to "explain" its input corpus (+ RL fine-tuning), which will likely contain relevant source code, documentation, papers, etc. to our problem. I'd also say that a piece of software is a theory too (quite literal…

The ai is just pattern matching. Vibing is not understanding, whether done by humans or machines. Vibe programmers (of which there are many) make a mess of the codebase piling on patch after patch. But they get the tests to pass!

Vibing gives you something like the geocentric model of the solar system. It kind of works but but it's much more complicated and hard to work with.

Re: Leanstral: Open-source agent for trustworthy coding and formal proof engineering

#158

Earlier quoted context omitted.

The scientific approach is not only or primarily empiricism. We didn't test our way to understanding. The scientific approach starts with a theory that does it's best to explain some phenomenon. Then the theory is criticized by experts. Finally, if it seems to be a promising theory tests are constructed. The tests can help verify the theory but it is the theory that provides the explanation which is the important par…

The theory still emanated from actual observations, didn't it ?

It did but they were meaningless without a human intellect trying to make sense of them.

Re: Leanstral: Open-source agent for trustworthy coding and formal proof engineering

#159

It’s great to see this pattern of people realising that agents can specify the desired behavior then write code to conform to the specs. TDD, verification, whatever your tool; verification suites of all sorts accrue over time into a very detailed repository of documentation of how things are supposed to work that, being executable, puts zero tokens in the context when the code is correct. It’s more powerful than ream…

> That’s because it encodes details, not intent.

Be careful here - make sure you encode the right details. I've seen many cases where the tests are encoding the details of how it was implemented and not what it is intended to do. This means that you can't refactor anything because your tests are enforcing a design. (refactor is changing code without deleting tests, the trick is how can you make design changes without deleting tests - which means you have to test as much as possible at a point where changing that part of the design isn't possible anyway)

Post reply on HN