Thread

Several vulnerabilities have been discovered in the Linux kernel

576 points · 408 comments · luispa

intrepidsoldier · 1790914300 · focus · HN ↗
Just the beginning. AI is going to expose how fragile the entire computing infrastructure in our world is.
1. jaypatelani · 1790916250 · focus · HN ↗
  Because most devs don't want to do formal verified system development. I know only one OS working on that which is open source Ironclad OS hope many others follow this path. It is Ada/SPARK based but others should do with whatever language they are using. NetBSD also heard going to do something similar with C in last AGM
  1. RossBencina · 1790920706 · focus · HN ↗
    > most devs don't want to do formal verified system development.
    That may be true. Serious question though: even if most devs wanted to develop formally verified code, do you think that it is reasonable to suggest that the typical systems developer could do it with today's tools? I don't mean verified protocols (TLA+) or verified algorithms (SPIN) I mean end-to-end verified code, a-la seL4. I got the impression that this is still very specialised work. Perhaps things have advanced since I last checked.

Unofficial Hacker News client; not affiliated with Y Combinator.