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

231–234 of 234 posts

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

#231

Post by markusde »

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…

In addition to Cedar:

[1] SymCrypt (MSR). Verified cryptographic primitives. It's in the latter style, using the Aeneas model of Rust.

[2] KLR (AWS). ML compiler. Not verified, but it's in the former style where they use pure Lean functions and interface with C code across the FFI.

[3] SampCert (AWS). Verified random sampling algorithms for differential privacy. Uses pure Lean functions and is called into via the reverse FFI.

Full disclosure I worked on 2 and 3 haha. There's also some stuff being used by cryptocurrency people but I don't follow that very closely.

[1] https://www.microsoft.com/en-us/research/blog/rewriting-symc... [2] https://github.com/leanprover/KLR [3] https://github.com/leanprover/SampCert

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

#232

Post by necovek »

bluGill wrote: post #227
necovek wrote: post #226

Earlier quoted context omitted.

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…

I am a bit perplexed at your claim that end-to-end tests are not fragile in general (my claim) with a counter how you spent a decade on not making them fragile in one particular case?

I am not disagreeing most projects evolve test suites which have duplicated, useless tests as a majority. But it can be done better.

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

#233

Post by bluGill »

necovek wrote: post #232
bluGill wrote: post #227

Earlier quoted context omitted.

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…

I am a bit perplexed at your claim that end-to-end tests are not fragile in general (my claim) with a counter how you spent a decade on not making them fragile in one particular case? I am not disagreeing most projects evolve test suites which have duplicated, useless tests as a majority. But it can be done better.

I have also spent a decade on some tiny unit tests that were fragile.

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

#234

Post by port11 »

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…

[dead]
Post reply on HN