Return Styles: Pseud0ch, Terminal, Valhalla, NES, Geocities, Blue Moon. Entire thread

seL4 formally verified microkernel

Name: Anonymous 2016-06-23 3:45

https://sel4.systems/

This is the kernel that flies the X-37 Orbital Test Vehicle. Why aren't you using it in your embedded programming?

Anyway, this got me thinking about formal verification. Is it overrated crap to suck out more research grant money, or is it worthwhile to learn and apply?

Does it make unit-testing look like something retarded drooling code-monkeys do?

It seems difficult to use in the real world. Can it be made simpler? What if everything was written with formal proofs?

Are dynamically typed languages impossible to automatically verify?

Name: Anonymous 2016-06-23 7:08

>>4
sure thing. but mathematical correctness doesn't prove it's completely bug-free. it means that if the assumptions are true, the implementation adheres to the specification. this allows for bugs if:
* specification contains logic flaws
* specification does not consider some special cases
* assumptions are not true

Newer Posts
Don't change these.
Name: Email:
Entire Thread Thread List