3 ms·

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

by ineol1 10y ago

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

Animats 10y ago
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 https://www.mpg.de/8746248/Foerderrichtlinien_Postdoc_en.pdf
- dikaiosune 10y ago
  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.
  - nickpsecurity 10y ago
    I agree. I regularly post the amazing work such people produce. A good example is Cyclone, which contributed to Rust's success.
  - semi-extrinsic 10y ago
    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.
- programLyrique 10y ago
  Are there lots of opportunities to work on static analysis and theorem proving outside academia, especially in Silicon Valley?
  - amenghra 10y ago
    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 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.
    - adrianN 10y ago
      > 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.

by ineol1 10y ago

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

Animats 10y ago

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 https://www.mpg.de/8746248/Foerderrichtlinien_Postdoc_en.pdf

dikaiosune 10y ago
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.
- nickpsecurity 10y ago
  I agree. I regularly post the amazing work such people produce. A good example is Cyclone, which contributed to Rust's success.
- semi-extrinsic 10y ago
  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.
programLyrique 10y ago
Are there lots of opportunities to work on static analysis and theorem proving outside academia, especially in Silicon Valley?
- amenghra 10y ago
  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 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.
  - adrianN 10y ago
    > 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.