2 ms·
Can't I just work on a subset of the language? I don't care if the linked list implementation I use isn't verified. I want to verify my own code, not because i
by Xmd5a 1y ago
Can't I just work on a subset of the language? I don't care if the linked list implementation I use isn't verified. I want to verify my own code, not because it will run on mars, but as an alternative to writing tests. Is this possible?
- 4ad 1y agoUnless you use a language designed for formal verification (Lean/Idris/Agda/F*/ATS/etc), no, it is not possible. You can get pretty far in Haskell (with various extensions) and Scala. But for Go/TypeScript/etc, forget about it.
- Jtsummers 1y agoYes. See SPARK for an example of this. It is a subset of Ada plus the SPARK portions to convey details and proofs. You can use it per file, not just on an entire program, which lets you prove properties of critical parts and leave the rest to conventional testing approaches.