thelamplighter_ (Jun 24 2026 at 15:58): thelamplighter_ (Jun 24 2026 at 15:58):Hey, I have been following Roc for some time now, and I really like that soft spot it occupies between the likes of Go lang and Rust lang, it sits in between, being really simple and friendly like Go as well as fast with nice performance, ergonomics, etc like Rust. It's like the best of both worlds, I have also been following Moonbit lang which for me also occupies that space too.
My question is on formal verification, is it something that would be featured in the Roc lang because I think with all the AI features for coding/programming, this really plays a good role in ensuring that a particular AI generated code is mathematically correct based on some constraints and I also think it creates an interesting workflow to work with AI in programming. I really love Roc by the way, majorly because of its simplistic nature but at the same time its not trading flexibility for simplicity like some other languages and secondly, the platform feature, I think its a nice approach to software decoupling (business logic from configuration and runtime, etc). Sadly its not ready yet for proper usage (i can't wait for v0.1).
Anton (Jun 24 2026 at 16:45):Thanks for the praise @thelamplighter_ :)
I'm not very familiar with formal verification but I could definitely see us experimenting with it sometime in the future. Relatedly, I follow Victor Taelin, he is working on rapid generation of provably correct programs.
thelamplighter_ (Jun 24 2026 at 16:52):I'm also not very versed with formal verification, but from what i understand after hearing about it from moonbit is that its a way to give constraints to a prover that proves that the code matches the constraints mathematically, more like an exhaustive amount of test cases. And moonbit lang supports this internally so you dont need to use an external system to verify the code. I think it will be really nice if Roc supports some form of builtin verification, because the simplicity of the language makes it easy for AI to generate workable code, then verification takes it a step further by allowing you give hard constraints to a prover to verify if the code generated works exactly as the constraints state.
thelamplighter_ (Jun 24 2026 at 16:54):its a fascinating topic I'm also exploring too, so funny, maybe in the future we just write constraints and the AI generates code and constantly tests that it is mathematically verified until it passes, maybe also combine snapshot testing or other forms of testing or even describe what we want and the AI generates its constraints and goes on like that.
thelamplighter_ (Jun 24 2026 at 17:08):Hey @Anton i just checked out Victor Taelin and the bend language, HVM runtime, and that is impressive, another rabbit hole to go down, thanks for the reference.
Anton (Jun 24 2026 at 17:09):I will definitely keep my eye on moonbit and what people are doing with their formal verification. Here is a related blog post for other interested readers: https://www.moonbitlang.com/blog/moonbit-0-9-release
Last updated: Jul 23 2026 at 13:15 UTC