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

221–230 of 234 posts

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

#221

Post by Eridrus »

isodev wrote: post #102
beernet wrote: post #26

Earlier quoted context omitted.

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.

> quality usually reigns over control and trust Most Copilot customers use Copilot because Microsoft has been able to pinky promise some level of control for their sensitive data. That's why many don't get to use Claude or Codex or Mistral directly at work and instead are forced through their lobotomised Copilot flavours. Remember, as of yet, companies haven't been able to actually measure the value of LLMs ... so it…

This too will be solved. You can get tye frontier models from AWS/Google/Azure without needing to send your data to anyone else already.

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

#222

Post by auggierose »

AlotOfReading wrote: post #219
auggierose wrote: post #183

Earlier quoted context omitted.

I think you have been confusing them. Two theorems are the same if they have the same statement (spec). A proof is not a theorem, nobody cares about when two proofs are the same or not.

Yes, and if you have the wrong theorems, the proof doesn't matter. Verification vs validation. Proofs solve verification, but the hard problem of validation remains.

> Yes, and if you have the wrong theorems, the proof doesn't matter.

Agreed.

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

#223

Post by d_christiansen »

cjfd wrote: post #113
trenchgun wrote: post #97

Earlier quoted context omitted.

>Such is very difficult at the moment What do you mean? It's a nice and simple language. Way easier to get started than OCaml or Haskell for example. And LLMs write programs in Lean4 with ease as well. Only issue is that there are not as many libraries (for software, for math proofs there is plenty). But for example I worked with Claude Code and implemented a shell + most of unix coreutils in like a couple of hours.…

Well, if you do not need to care about performance everything can be extremely simple indeed. Let me show you some data structure in coq/rocq while switching off notations and diplaying low level content. Require Import String. Definition hello: string := "Hello world!". Print hello. hello = String (Ascii.Ascii false false false true false false true false) (String (Ascii.Ascii true false true false false true true f…

In Lean, strings are packed arrays of bytes, encoded as UTF-8. Lean is very careful about performance; after all, a self-hosted system that can't generate fast code would not scale.

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

#224

Post by d_christiansen »

wazHFsRy wrote: post #214
markusde wrote: post #161

Earlier quoted context omitted.

Also a very good question btw, people do both. For some projects Lean is expressive and performant enough to use on its own (or call into using the reverse FFI), other projects use a model of a real programming language like Rust. The disadvantage of the latter is that the Lean model of Rust has to be trusted.

Do you know if there are some resources or examples of this? Especially actual production stuff, not just side projects or proof of concepts?

Cedar (https://lean-lang.org/use-cases/cedar/) at AWS use an executable Lean model of a system as an oracle for differential testing of a Rust implementation. If you can't run Lean in production, then their approach is compelling.

The idea is that you start with a Lean specification, create a fully verified implementation with respect to the spec, and then hook it and the production implementation up to a fuzzer or source or random inputs. Then you can explore a lot of the state space fully automatically.

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

#225

Post by justboy1987 »

d_christiansen wrote: post #224
wazHFsRy wrote: post #214

Earlier quoted context omitted.

Do you know if there are some resources or examples of this? Especially actual production stuff, not just side projects or proof of concepts?

Cedar ( https://lean-lang.org/use-cases/cedar/ ) at AWS use an executable Lean model of a system as an oracle for differential testing of a Rust implementation. If you can't run Lean in production, then their approach is compelling. The idea is that you start with a Lean specification, create a fully verified implementation with respect to the spec, and then hook it and the production implementation up to a fuzzer or…

[flagged]

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

#226

Post by necovek »

bluGill wrote: post #210
necovek wrote: post #203

Earlier quoted context omitted.

While you are right that you need to be encoding the right details, I disagree on the tests enforcing a design point. As part of the proper testing strategy, you will have tests that cover individual behavior of a small block/function (real "unit" tests), tests that cover integration points only up to the integration itself, and a small number of end-to-end or multi-component integration tests. Only the last category…

Fine, but don't check in the tests that prove implementation since they will be deleted soon anyway. The only tests to check in are ones that - by failing - informed you that you broke something. We don't know which those tests are and because most tests run fast we tend to check in lots of tests that will never fail in a useful way.

Taken to its logical conclusion, what you are saying is do not write (or commit? but in practice, why write them if not to run in CI) any tests except for end-to-end tests covering actual use cases. In theory, even make them generic enough so they are not affected by the implementation. Perhaps even employ LLMs there ("check that a customer can provide their address for their order by using a headless browser").

It is a strong disagree from me: end-to-end tests have always been fragile and slow, and feedback loop time is the boundary at which any coder (agentic or human) needs to operate on. If your agents need to wait 2h to see if their every change is valid, you'll be beat by humans doing properly structured "just enough" testing.

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

#227

Post by bluGill »

necovek wrote: post #226
bluGill wrote: post #210

Earlier quoted context omitted.

Fine, but don't check in the tests that prove implementation since they will be deleted soon anyway. The only tests to check in are ones that - by failing - informed you that you broke something. We don't know which those tests are and because most tests run fast we tend to check in lots of tests that will never fail in a useful way.

Taken to its logical conclusion, what you are saying is do not write (or commit? but in practice, why write them if not to run in CI) any tests except for end-to-end tests covering actual use cases. In theory, even make them generic enough so they are not affected by the implementation. Perhaps even employ LLMs there ("check that a customer can provide their address for their order by using a headless browser"). It i…

That isn't the logical conclusion though. I specificly said find places where change would be too complex to attempt anyway which breaks your conclusion. This lets you find plenty of places to jump in and write a test. (You will still be wrong but less often and generally you know it will be a hard change before you start making it)

though I find in practice end to end tests are not that fragile. It took us a decade of effort to find and mitigate all the little issues that make them fragile though so perhaps you don't want to go that far. I wish I could make the end to end tests faster though, but fragile they are not.

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

#228

Post by KetoManx64 »

segmondy wrote: post #51
beernet wrote: post #26

Earlier quoted context omitted.

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.

Ha, keep putting your prompts and workflows into cloud models. They are not okay with being a platform, they intend to cannibalize all businesses. Quality doesn't always reign over control and trust. Your data and original ideas are your edge and moat.

The same old speech that has been used throughout history. When cars were invented people complained to everyone that Ford intended to cannbolize all horse drawn carriages. When manufacturing was invented it cannibalized the work of all the sewing and knitting companies that had women making one item at a time. When Google was invented it cannabolized libraries, and encyclopedias, etc. etc. Yet nobody wants a horse drawn carriage, nor to knit their own sweaters, nor go to the library to look things up in a physical encyclopedia.

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

#229

Post by disgruntledphd2 »

Aerroon wrote: post #192
disgruntledphd2 wrote: post #156

Earlier quoted context omitted.

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 com…

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

As I said, the core of the AI act was written about supervised ML, not generative ML, as generative ML wasn't as big a deal pre Chat GPT.

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

As I also said, the foundation model stuff (including this flops thing) is incredibly stupid. I agree with you on this, but my point is that the core of the AI act was supposed to cover the ML systems built since approx 2010.

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

Again, you're talking about generative stuff (makes sense given the absurdly misleading name now) whereas I'm talking about the original AI act, which I read well before ChatGPT happened.

The training data thing is a tradeoff, like copyright is far too invasive (IMO) and it's good to be able to use this information for other purposes. However, I personally would be super worried about an ML team that couldn't tell me what data went into their model. Like, the data is core to all ML/AI approaches so that lack of understanding would make me very sceptical of any performance claims.

Lets be real, the AI companies don't want to say what's in their models because of the rampant copyright infringement, not because of any technical incapability.

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

#230

Post by casey2 »

I get why the massive roll out is happening, but it's still possible that everything LLMs are good for can be done on the cheap. It's just another point for Google's multimodal focus.

I think in 10 years most providers will implode because they can't justify the debt for a cheap commodity product. While Google (and probably OpenAI) will have a huge moat due to users/multimodal/world models

Post reply on HN