4 ms·

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 spec

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.

kevlar700 2y ago
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.
- LiamPowell 2y ago
  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/abaaa1f84827a1d81bcdb2f5f1743406 https://gist.github.com/liampwll/abaaa1f84827a1d81bcdb2f5f17...
  - xxpor 2y ago
    p4? Granted, that's not something that just compiles to a usable language.
TheOtherHobbes 2y ago
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.
steveklabnik 2y ago
> 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.
siknad 2y ago
Maybe better performance can be achieved with specialized models. There are some that were able to solve mathematical olympiad problems, e.g. AlphaProof.

kevlar700 2y ago

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.

LiamPowell 2y ago
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/abaaa1f84827a1d81bcdb2f5f1743406 https://gist.github.com/liampwll/abaaa1f84827a1d81bcdb2f5f17...
- xxpor 2y ago
  p4? Granted, that's not something that just compiles to a usable language.

TheOtherHobbes 2y ago

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.

steveklabnik 2y ago

> 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.

siknad 2y ago

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