Hacker News Reader

Comment by stefan_ | Hacker News Reader

Have you tried it for Rust, arguably a much lower bar than actually fully formally verifiable? Sorry to say but AI can't figure out the borrow checker. I'd speculate it does poor on a lot of things that are sort of implicit in the code / properties of the grand structure rather than incremental text things.

View on HN

There is a podcast and blackhat? video about Nvidia choosing SPARK over Rust. Not because of formal verification at all but because it is a more developed prospect and offers better security even without any formal verification. This isn't mentioned but Ada is also far better at modelling registers or even network packets.

I might consider AI if it utilised SPARKs gnat prove but I wouldn't usw AI otherwise.

As an example of modelling packets, here's an example of modelling a complex packet which is a bit-packed tagged union. I don't think many other languages make such packets so easy to declare: https://gist.github.com/liampwll/abaaa1f84827a1d81bcdb2f5f17...

p4? Granted, that's not something that just compiles to a usable language.

Maybe better performance can be achieved with specialized models. There are some that were able to solve mathematical olympiad problems, e.g. AlphaProof.

AI means some future more rigorous system than today's Clippy++ LLMs.

At least that's what it should mean. It's not clear if that's going to happen.

> Sorry to say but AI can't figure out the borrow checker. I'd speculate it does poor on a lot of things that are sort of implicit in the code / properties of the grand structure rather than incremental text things.

I don’t really use AI tools, but in the past few weeks I’ve tried it with Rust and while it had problems, borrow checking errors were never part of them.

I fully agree that LLMs don’t “understand,” but people also really oversell the amount of thinking needed to satisfy borrowing in a lot of cases.

Reply on news.ycombinator.com