8 ms·
"the project has 711 times as much test code and test scripts" than source code. That's a really impressive feat.
by fuddle 8y ago
"the project has 711 times as much test code and test scripts" than source code. That's a really impressive feat.
- deleted 8y ago[deleted]
- monocasa 8y agoHuh, at that point it'd probably make more sense to formally verify it. For sel4 last time I checked the ratio was 25/1 proof code/verified code.
- sudeepj 8y agoAs far as I understand, formal verification does not certify the implementation even though the algorithms used are sound.
- geofft 8y agoIt depends—many proof-assistant languages let you extract an implementation directly out of your formally-specified algorithm (generally by dropping rich typing-ish information, but you've already verified it's correct). Or take seL4, which amazingly proves that not just the C code but also the binary faithfully matches their formally-specified algorithms. https://sel4.systems/Info/FAQ/proof.pml https://sel4.systems/Info/FAQ/proof.pml Of course who knows what your CPU microcode is doing, but for the question at hand—ensuring a highly portable C library does what it claims to do more efficiently and accurately than exhaustive testing—formal verification is certainly a reasonable approach.
- krylon 8y agoSQLite is used on many platforms, built using many compilers. All of those compilers might have bugs themselves (who am I kidding? They do), something verification cannot account for.