Hacker News Board Hacker News, browsed like a classic message board
Live data from Hacker News

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

mistral.ai

Post reply on HN
Print view View original

141–150 of 234 posts

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

#141

Post by ptidhomme »

discreteevent wrote: post #129
chriswarbo wrote: post #127

Earlier quoted context omitted.

Tests (and type-checkers, linters, formal specs, etc.) ground the model in reality: they show it that it got something wrong (without needing a human in the loop). It's empiricism, "nullius in verba"; the scientific approach, which lead to remarkable advances in a few hundred years; that over a thousand years of ungrounded philosophy couldn't achieve.

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 ?

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

#142

Post by pydry »

chriswarbo wrote: post #127
BowBun wrote: post #77

Earlier quoted context omitted.

I feel like the difference is minimal, if not entirely dismissable. Code in this sense is just a representation of the same information as someone would write in an .md file. The resolution changes, and that's where both detail and context are lost. I'm not against TDD or verification-first development, but I don't think writing that as code is the end-goal. I'll concede that there's millions of lines of tests that a…

Tests (and type-checkers, linters, formal specs, etc.) ground the model in reality: they show it that it got something wrong (without needing a human in the loop). It's empiricism, "nullius in verba"; the scientific approach, which lead to remarkable advances in a few hundred years; that over a thousand years of ungrounded philosophy couldn't achieve.

This assumes that tests are realistic, which for the most part they are not.

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

#143

Post by warpspin »

kimsant wrote: post #121

AI agents will become a comodity. Europeans not wanting to be dependent, and they are giving for free what US investors planed to charge with 90% margin. Amazing! What a blast. Thank you for your service (this first 100M$ burned to POC GPT1 and from here, we are so good to go)

The problem with the European independence story is, that it seems Mistral runs its own stuff also on US cloud act affected infrastructure. This makes them a very weird value proposition: If I accept a level of "independence" whereby I run on AWS or Azure, I could as well pay for Anthropic or GPT to have SOTA performance.

If I do not accept that level of independence but want more, I need to buy what's on OVH, Scaleway, Ionos etc. or host my own, but that usually means even smaller, worse models or a lot of investment.

Nevertheless, the "band" that Mistral occupies for economic success is very narrow. Basically just people who need independence "on paper" but not really. Because if I'm searching for actual independence, there's no way I could give them money at the moment for one of their products and it making sense, cause none of their plans are an actual independence-improvement over, let's say, Amazon Bedrock.

I really really want to support them, but it must make economic sense for my company, too, and it doesn't.

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

#144

Post by pydry »

nextos wrote: post #82
tonymet wrote: post #74

Earlier quoted context omitted.

AI is the reality that TDD never before had the opportunity to live up to

Not just TDD. Amazon, for instance, is heading towards something between TDD and lightweight formal methods. They are embracing property-based specifications and testing à la Haskell's QuickCheck: https://kiro.dev Then, already in formal methods territory, refinement types (e.g. Dafny, Liquid Haskell) are great and less complex than dependent types (e.g. Lean, Agda).

The deluge of amazon bugs ive been seeing recently makes me hesitant to follow in amazon's lead.

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

#146

Post by hrmtst93837 »

beernet wrote: post #26
jasonjmcghee wrote: post #8

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

Agreed. The idea is nice and honorable. At the same time, if AI has been proving one thing, it's that quality usually reigns over control and trust (except for some sensitive sectors and applications). Of course it's less capital-intense, so makes sense for a comparably little EU startup to focus on that niche. Likely won't spin the top line needle much, though, for the reasons stated.

[flagged]

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

#147

Post by chriswarbo »

discreteevent wrote: post #129
chriswarbo wrote: post #127

Earlier quoted context omitted.

Tests (and type-checkers, linters, formal specs, etc.) ground the model in reality: they show it that it got something wrong (without needing a human in the loop). It's empiricism, "nullius in verba"; the scientific approach, which lead to remarkable advances in a few hundred years; that over a thousand years of ungrounded philosophy couldn't achieve.

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 literally, if we follow Curry-Howard). A piece of software generated by an LLM is a more-specific, more-explicit subset of its internal NN model.

Tests, and other real CLI interactions, allow the model to find out that it's wrong (~empiricism); compared to going round and round in chain-of-thought (~philosophy).

Of course, test failures don't tell us how to make it actually pass; the same way that unexpected experimental/observational results don't tell us what an appropriate explanation/theory should be (see: Dark matter, dark energy, etc.!)

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

#148

Post by benterix »

teekert wrote: post #110
andai wrote: post #3

Trustworthy vibe coding. Much better than the other kind! Not sure I really understand the comparisons though. They emphasize the cost savings relative to Haiku, but Haiku kinda sucks at this task, and Leanstral is worse? If you're optimizing for correctness, why would "yeah it sucks but it's 10 times cheaper" be relevant? Or am I misunderstanding something? On the promising side, Opus doesn't look great at this benc…

I also don't understand the focus on vibe coding in the marketing. Vibe coding kind of has the image of being for non-devs, right? I do like agents (like Claude Code), but I don't consider myself to be vibe coding when I use them. Either I'm using a language/framework I know and check every step. OR I'm learning, checking every step and asking for explanations. I tried vibe coding, and really dislike the feeling I ha…

> I tried vibe coding, and really dislike the feeling I have when doing it. It feels like building a house, but without caring about it, and just using whatever tech. Sure I may have moisture problems later, but it's a throwaway house anyway. That's how I feel about it. Maybe I have a wrong definition.

No, I feel the same. I vibe-coded a few projects and after a few weeks I just threw them away, ultimately I felt I just wasted my time and wished I coudl get it back to do something useful.

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

#149

Post by cowboy_henk »

chriswarbo wrote: post #127
BowBun wrote: post #77

Earlier quoted context omitted.

I feel like the difference is minimal, if not entirely dismissable. Code in this sense is just a representation of the same information as someone would write in an .md file. The resolution changes, and that's where both detail and context are lost. I'm not against TDD or verification-first development, but I don't think writing that as code is the end-goal. I'll concede that there's millions of lines of tests that a…

Tests (and type-checkers, linters, formal specs, etc.) ground the model in reality: they show it that it got something wrong (without needing a human in the loop). It's empiricism, "nullius in verba"; the scientific approach, which lead to remarkable advances in a few hundred years; that over a thousand years of ungrounded philosophy couldn't achieve.

This only holds if you understand what's in the tests, and the tests are realistic. The moment you let the LLM write the tests without understanding them, you may as well just let it write the code directly.

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

#150

Post by kimsant »

warpspin wrote: post #143
kimsant wrote: post #121

AI agents will become a comodity. Europeans not wanting to be dependent, and they are giving for free what US investors planed to charge with 90% margin. Amazing! What a blast. Thank you for your service (this first 100M$ burned to POC GPT1 and from here, we are so good to go)

The problem with the European independence story is, that it seems Mistral runs its own stuff also on US cloud act affected infrastructure. This makes them a very weird value proposition: If I accept a level of "independence" whereby I run on AWS or Azure, I could as well pay for Anthropic or GPT to have SOTA performance. If I do not accept that level of independence but want more, I need to buy what's on OVH, Scalew…

I don’t care about the servers, they are a comodity already.

The key is to avoid chantage, remember Oracle with DBs, people learned not to build on top of unreplaceable stuff

Post reply on HN