> Word is out, and unfortunately true: @CSIRO's @Data61news dismantles Trustworthy Systems (TS), the team that shook the scientific world with the first correctness proof of an OS, #seL4. TS staff to reallocate to AI projects or sacked.
> TS was exemplary in @CSIRO's @Data61news: from world-leading fundamental research to real-world deployment. It had a strong culture of excellence that aimed high and shunned incremental work, #seL4 a prime example. @sel4Foundation
> Claims by @CSIRO's @Data61news of research excellence sound hollow. I challenge you to identify work in Data61 eclipsing the TS team and #seL4. Yet it's easy to identify highly incremental work in Data61 that seems safe.
> And it's not that TS rested on its laurels: Time Protection, systematic prevention of information leakage through timing channels - in the too-hard basket for most. This has just won its third Best Paper Award, at @DateConference'21.
> This would be a disaster for #seL4, had we not set up the seL4 Foundation to minimise dependency on @CSIRO's @Data61news. Please help us strengthening @seL4Foundation, to bring real #security to the world's computing systems.
> TS's work will continue @UNSW, in close collaboration with @lsf37 and colleagues at #ProofCraft and our ecosystem partners in @seL4Foundation. Together we will continue to define the state of the art in OS #security.
People with no scientific knowledge get to apply their own very personal and informed view on what to fund: AI (and infosec apparently). Nice move, funnel money to startups and the big sharks (vc and other), move publicly funded research to corporate territory. If only they would allocate their funds originally (what they would call "distruptively" right?), i would be ok.
