Hacker News Reader

Comment by ineol1 | Hacker News Reader

Derek Dreyer and collaborators are working on specifying what needs to be proven about unsafe code, see http://plv.mpi-sws.org/rustbelt/

View on HN

That's good. They may have trouble recruiting. They're looking for people who could make upwards of $150K in Silicon Valley and want to pay them at postdoc rates. Glassdoor says €41,595. Their own material has even lower rates.[1]

[1] https://www.mpg.de/8746248/Foerderrichtlinien_Postdoc_en.pdf

That's just the status quo for postdocs and PhD students, AFAICT. And yet universities everywhere still find people to take them up on the deal.

I agree. I regularly post the amazing work such people produce. A good example is Cyclone, which contributed to Rust's success.

Well, the academic and implementation-wise freedoms are huge compared to any SV startup. And you don't need to worry much about financials, nor marketing, nor a million other things that many hackers dislike.

Are there lots of opportunities to work on static analysis and theorem proving outside academia, especially in Silicon Valley?

Static analysis: for sure. Companies with large codebases are interested to understand how their code works, build refactoring tools, find bugs, etc. They have dedicated teams doing this. For example https://github.com/facebook/pfff.

Formal proofs: there are specific applications (see Amazon's use of TLA+). I personally feel nearly every company has a small piece of code that you can justify spending a few weeks/months modeling to ensure its correctness. Also, engineers working on medical devices, avionics, robotics, finance, etc. probably get to prove the correctness of their code.

> Also, engineers working on medical devices, avionics, robotics, finance, etc. probably get to prove the correctness of their code.

Some might, but the relevant ISO standards are ok with testing if you reach sufficient coverage, so generally testing is all that's happening.

Reply on news.ycombinator.com