3 ms·
I think the seL4 kernel rather proves that you can write safe haskell, verify it, and then transpile that to C. That's different from directly writing C...
by jabot 9y ago
I think the seL4 kernel rather proves that you can write safe haskell, verify it, and then transpile that to C.
That's different from directly writing C...
- sanxiyn 9y agoWell, you aren't directly writing C anyway. Unless you are https://xkcd.com/378/ https://xkcd.com/378/ -- using tools is perfectly okay. Anyway, PolarSSL is definitely not transpiled. Its source language is C.
- jabot 9y agohttp://www.cvedetails.com/vulnerability-list/vendor_id-12001/product_id-22470/year-2015/opec-1/Polarssl-Polarssl.html http://www.cvedetails.com/vulnerability-list/vendor_id-12001... ... and your point is? EDIT: more recent bugs: https://tls.mbed.org/security https://tls.mbed.org/security These bugs include double-free and use-after-free - which are not covered by the original analysis, right?
- agumonkey 9y agoin the end the idea is that if you are semantic aware, then everything is safe; it's just operations from exp -> env -> store to env -> store etc etc
- nine_k 9y agoIndeed! You can write safe programs for e.g. the original Turing Machine. But I bet you'll end up writing tools to make creating a safe program of any non-trivial size feasible. A large class of these tools is usually called "programming languages".