Re:Some notes on Rust, mutable aliasing and formal verification
by worik on Thursday May 16, 2024 @08:08PM
(#40384907)
Yes.
I am not against all formal methods. Pre and post conditions for loops etcetera. When they are useful they should be used (in many cases they are built in: `for i = k; i < l; i++` has a precondition, a loop condition, and an action all in one statement.)
It is the idea, that was very hot thirty or so years ago, that by using formal specifications and rules of inference we could eliminate bugs.
I am not against all formal methods. Pre and post conditions for loops etcetera. When they are useful they should be used (in many cases they are built in: `for i = k; i < l; i++` has a precondition, a loop condition, and an action all in one statement.)
It is the idea, that was very hot thirty or so years ago, that by using formal specifications and rules of inference we could eliminate bugs.