3 ms·
I think the problem with the PLT space is that it's not monetizable the same way that e.g. ML is. If you get a Ph.D in ML, you have an easy shot at a high payin
by lambdasquirrel 5y ago
I think the problem with the PLT space is that it's not monetizable the same way that e.g. ML is. If you get a Ph.D in ML, you have an easy shot at a high paying industry job. Not so with a Ph.D in PLT. That alone provides some force for research.
It's hard getting enough investment in the PLT space because the costs that are borne can't be easily recouped. It's a classic problem with research. And we know how much the world runs around money right now.
- pjmlp 5y agoNowadays, 30 years ago my AI professors where trying to keep their classes open and stuff like neural networks where optional lectures.
- oxff 5y agoQuick, easy formal verification tools that programmers can use on the spot from the IDE are hard to make for most languages because most languages and their compilers weren't made with such thing in mind. I guess Rust might be heading somewhere interesting with tooling, with tools like Flowistry existing (https://github.com/willcrichton/flowistry https://github.com/willcrichton/flowistry) showing what is possible. It's a plugin that can compute backwards / forwards static slices for you, straight in the IDE as a VSCode plugin. I think you need an external program that runs a full program analysis to do the same in C++.
- pjmlp 5y agoFrama-C and Ada/SPARK are two examples of tooling with IDE support and wide use in high integrity computing domain.