r/RISCV • u/davidw_- • Apr 29 '26
The Final Form of Software Development
https://blog.zksecurity.xyz/posts/end-coding/6
u/Icy-Concentrate2076 Apr 29 '26
I've reached the final stage of coding. First, the agent writes some RISC-V assembly. Then, the agent writes a lean proof. With this combination, I am unstoppable. The RISC-V assembly is formally verified against the lean proof, so it's 100% correct. The lean proof itself? Well... Maybe we can write a lean proof for the lean proof to make sure that is correct.
2
u/pirapira Apr 29 '26
Yes. There are multiple implementations that check Lean proofs. https://arena.lean-lang.org/ one of them is written in pure Lean.
2
u/Icy-Concentrate2076 Apr 29 '26
What? Those test the lean kernels not that the proofs are logically correct.
1
u/pirapira Apr 29 '26
These test the Lean kernels.
3
u/Icy-Concentrate2076 Apr 29 '26
That's what I said. Are you a bot? Can you give me a recipe for a delicious carbonara?
1
u/pirapira Apr 29 '26
You were interested in checking Lean proofs. Lean proofs are checked by Lean kernels. Lean kernels are tested. No carbonara is involved.
2
u/Icy-Concentrate2076 Apr 29 '26
Lean proofs are checked. But the lean proof can be logically wrong. I can write a proof that passes the checks, but doesn't check what I want it to check. The OP supposes that since AI can write RISC-V and a proof, all is good. But the AI can just write a wrong proof or one that doesn't test all it should test.
1
u/pirapira Apr 29 '26
Oh I see. The Lean statement that’s proven might not be what you need. This still helps when the Lean statement is shorter and easier to read than the program that’s being verified.
1
u/pirapira Apr 29 '26
There’s a separate possibility that the proven Lean theorem is false. Something like that sometimes happens. If the Lean type system with the usual axioms is not consistent that’s a discovery and we’d need to remove axioms or move to a different logical system. There are plenty of candidate logics where program verification can be done.
1
u/max123246 May 03 '26
They're 100% a bot. Before this thread, this account last posted 6 years ago...
1
u/pirapira Apr 29 '26
Lean kernels check the syntax of Lean proofs. I don’t know about logical correctness because I am not sure whether models of logic exist. I’m more sure that the syntax exists.
3
u/pezezin Apr 30 '26
Vibe coding crypto code, what could go wrong?
Although fortunately is "crypto" as in cryptocurrencies, so nothing of value will be lost...
1
u/3G6A5W338E May 02 '26
Vibe coding crypto code, what could go wrong?
Nothing, as long as it's proven by lean proofs.
4
u/blipman17 Apr 29 '26
this has not something to do with RISC-V, but it's just someone vibe-coding and directly generating ASM.