Hacker News Reader

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...

in 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

Indeed! 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".

Well, you aren't directly writing C anyway. Unless you are https://xkcd.com/378/ -- using tools is perfectly okay.

Anyway, PolarSSL is definitely not transpiled. Its source language is C.

http://www.cvedetails.com/vulnerability-list/vendor_id-12001...

... and your point is?

EDIT: more recent bugs:

https://tls.mbed.org/security

These bugs include double-free and use-after-free - which are not covered by the original analysis, right?

Reply on news.ycombinator.com