[dead]
Leanstral: Open-source agent for trustworthy coding and formal proof engineering
131–140 of 234 posts
Re: Leanstral: Open-source agent for trustworthy coding and formal proof engineering
#132Earlier 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.
It most certainly is not. All your tests are doing is seeding the context with tokens that increase the probability of tokens related to solving the problem being selected next. One small problem: if the dataset doesn't have sufficiently well-represented answers to the specific problem, no amount of finessing the probability of token selection is going to lead to LLMs solving the problem. The scientific method is grounded in the ability to reason, not probabilistically retrieve random words that are statistically highly correlated with appearing near other words.
Re: Leanstral: Open-source agent for trustworthy coding and formal proof engineering
#133AI 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)
they will, but the jagged frontier is fractal and each one will have different capabilities; you'll want to mix models and to get best results consistently you'll need to.
Re: Leanstral: Open-source agent for trustworthy coding and formal proof engineering
#134It’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…
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 back to your codebase space, you've got yourself a huge unlock. (spoiler alert: you basically can, today)
Re: Leanstral: Open-source agent for trustworthy coding and formal proof engineering
#135Earlier quoted context omitted.
If Agent is writing the tests itself, does it offer better correctness guarantees than letting it write code and tests?
Given the issues with AWS with Kiro and Github, We already have just a few high-profile examples of what happens when AI is used at scale and even when you let it generate tests which is something you should absolutely not do. Otherwise in some cases, you get this issue [0]. [0] https://sketch.dev/blog/our-first-outage-from-llm-written-co...
Don't "let it" generate tests. Be intentional. Define them in a way that's slightly oblique to how the production code approaches the problem, so the seams don't match. Heck, that's why it's good to write them before even thinking about the prod side.
Re: Leanstral: Open-source agent for trustworthy coding and formal proof engineering
#136Earlier 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…
I wonder what the biggest (non-AI) moats are for US tech against the alternatives?
[dead]
Re: Leanstral: Open-source agent for trustworthy coding and formal proof engineering
#137Earlier 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…
> It feels like building a house, but without caring about it, and just using whatever tech. So, most homebuilders (in the US) unfortunately.
I myself am now and expert at insulation and all the vapor-permeable and vapor-blocking membranes/foils/foams that come with it.
It came at great cost though, I hated the process of learning and the execution. I was less than happy for some years. But I feel even more uncomfortable vibe-home-improving than I do vibe-coding. The place is starting to look nice now though.
Re: Leanstral: Open-source agent for trustworthy coding and formal proof engineering
#138lol, why does the paper abstract assume I know what Lean is and it goes on to talk about lean 4 improvements?
Why do you expect to understand an article you randomly read off the interwebs?
Re: Leanstral: Open-source agent for trustworthy coding and formal proof engineering
#139AI 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)
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?
Re: Leanstral: Open-source agent for trustworthy coding and formal proof engineering
#140Curious 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]