3 ms·

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 prosp

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.