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

191–200 of 234 posts

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

#191

Post by xpe »

Public service announcement to hopefully reduce unnecessary knife fights*:

There are two compatible and important (but different) questions in play:

1. Is a program correct relative to a formal specification?

2. Is the formal specification what we mean/want?

*: Worth asking: “What that other person necessarily wrong? Or perhaps they are discussing a different aspect or framing?” AKA: “be curious and charitable” I’m not going to link to the specific threads, but they are happened / are happening. Le Sigh.

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

#192

Post by Aerroon »

disgruntledphd2 wrote: post #156
Aerroon wrote: post #90

Earlier quoted context omitted.

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.

>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.

It's not an excuse. Anybody with half a working brain should've been able to tell that this was going to happen. You can't regulate a field in its infancy and expect it to ever function.

>The compliance burden falls mostly on the companies big enough to handle it.

You mean it falls on anyone that tries to compete with a model. There's a random 10^25 FLOPS compute rule in there. The B300 does 2500-3750 TFLOPS at fp16. 200 of these can hit that compute number in 6 months, which means that in a few years time pretty much every model is going to hit that.

And if somebody figures out fp8 training then it would only take 10 of these GPUs to hit it in 6 months.

The copyright rule and having to disclose what was trained on also means that it will be impossible to have enough training data for an EU model. And this even applies to people that make the model free and open weights.

I don't see how it is possible for any European AI model to compete. Even if these restrictions were lifted it would still push away investors because of the increased risk of stupid regulation.

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

#194

Post by refulgentis »

Paracompact wrote: post #89
refulgentis wrote: post #79

Earlier quoted context omitted.

But isn't that tantamount with "his comment is a complete non-sequitor"?

I don't think so? Lean is formal methods, so it makes sense to discuss the boons of formal and semiformal methods more generally. I used to think that the only way we would be able to trust AI output would be by leaning heavily into proof-carrying code, but I've come to appreciate the other approaches as well.

But that's exactly my point. "It's natural to discuss the broader category" is doing a lot of heavy lifting here. The blog post is making a very specific claim: that formal proof, checked by Lean's kernel, is qualitatively different from testing, it lets you skip the human review loop entirely. cadamsdotcom's comment rounds that down to "executable specs good, markdown specs bad," which... sure, but that's been the TDD elevator pitch for 20 years.

If someone posted a breakthrough in cryptographic verification and the top comment was "yeah, unit tests are great," we'd all recognize that as missing the point. I don't think it's unrelated, I think it's almost related, which is worse, because it pattern-matches onto agreement while losing the actual insight.

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

#196

Post by teekert »

andai wrote: post #188
teekert wrote: post #110

Earlier quoted context omitted.

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…

Yeah, the original meaning of Vibe Coding was "not looking at the code, just going on vibes", but a lot of people now use it to mean "AI was involved in some way". I see a whole spectrum between those two. I typically alternate between "writing code manually and asking AI for code examples" (ChatGPT coding), and "giving AI specific instructions like, write a function blarg that does foo". The latter I call Power Codi…

"I don't hear a lot of people doing this though? Maybe we just don't have good language for it."

Interesting thought. I guess we don't really, vibe coding is to powerful a term. But perhaps just call it LLM assisted programming? Where we used to do Stack Overflow assisted programming. LLM assisted programming is more focused, goes faster. But since you're wandering around less I guess you learn less, you're exposed to less new information, some of it was helpful in unexpected ways. Now you have to make learning a specific part of your flow, and that takes discipline/time. But is well worth it imho. Actually, for me it's the only way to enjoy it.

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

#197

Post by coffeebeqn »

utopiah wrote: post #139
bigfudge wrote: post #125

Earlier quoted context omitted.

I really hope you're right. Sadly, though, I don't see any evidence of UK companies disinvesting from big US tech. There aren't good alternatives and what there is is too complex. As long as 'everyone else is still using MS', it seems like it's a brave CTO that switches to European providers. Unless that happens, the network effect of having AI+data is likely to mean US tech still has a big advantage in corp settings…

> There aren't good alternatives and what there is is too complex. Sounds like a worth challenge for this community, mind giving actual examples and see what others can suggest?

Vertical integration and breadth and depth of offerings on the cloud and customer lock-in from dominating it for 20 years

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

#199

Post by refulgentis »

baq wrote: post #134
refulgentis wrote: post #70

Earlier quoted context omitted.

I've seen this sentiment and am a big fan of it, but I was confused by the blog post, and based on your comment you might be able to help: how does Lean help me? FWIW, context is: code Dart/Flutter day to day. I can think of some strawmen: for example, prove a state machine in Lean, then port the proven version to Dart? But I'm not familiar enough with Lean to know if that's like saying "prove moon made of cheese wit…

yesterday I had to tell a frontier model to translate my code to tla+ to find a tricky cache invalidation bug which nothing could find - gpt 5.4, gemini 3.1, opus 4.6 all failed. translation took maybe 5 mins, the bug was found in seconds, total time to fix from idea to commit - about 15 mins. if you can get a model to quickly translate a relevant subset of your code to lean to find tricky bugs and map lean fixes bac…

Thanks for following up on this: I was really surprised by how much air this paeon to, idk, TDD, took out of the comments by getting off-topic.

Before you commented, I started poking at what you described for 15 minutes, then forget about it and fell asleep. Now I remembered, and I know it's viable and IIUC it's almost certainly going to make a big difference in my work practice moving forward. Cheers.

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

#200

Post by cadamsdotcom »

vidarh wrote: post #119
cadamsdotcom wrote: post #112

Earlier quoted context omitted.

Say you describe your kitchen as “I want a kitchen” - where are the knives? Where’s the stove? Answer: you abdicated control over those details, so it’s wherever the stochastic parrot decided to put them, which may or may not be where they ended up last time you pulled your LLM generate-me-a-kitchen lever. And it may not be where you want. Don’t like the layout? Let’s reroll! Back to the generative kitchen agent for…

If it is fast enough, and cheap enough, people would very happily reroll specific subsets of decisions until happy, and then lock that down . And specify in more details the corner cases that it doesn't get just how you want it. People metaphorically do that all the time when designing rooms, in the form of endless browsing of magazines or Tik Tok or similar to find something they like instead of starting from first…

Agreed; often you don’t know quite what you want until you’ve seen it.

Spec is an overloaded term in software :) because there are design specs (the plan, alternatives considered etc) and engineering style specs (imagine creating a document with enough detail that someone overseas could write your documentation from it while you’re building it)

Those need distinct names or we are all at risk of talking past each other :)

Post reply on HN