Hacker News new | past | comments | ask | show | jobs | submit login

I do pure type theory, semantics, proof theory & intuitionistic mathematics. Very little of this will find a home in industry (at least, not for several decades). Industry has historically been incredibly resistant to 100% of the things I'm interested in, and I don't blame them!

But it's not just the hard & expensive stuff that they are resistant to. Even the "easy" stuff (like adopting a programming language designed by the professionals instead of the amateurs) they won't do.

I build interactive proof assistants. But I'm not pushing their applicability to industry, and I don't expect them to be relevant to industry (for a long time at least). Why? Because it's too expensive. Formal verification in type theory MAKES NO ECONOMIC SENSE; ask anyone who's actually ever done any industrial verification, and you will find out what tools they are using, and it has nothing at all to do with the area of research I'm involved in. This is because there are inherent trade-offs in every technique, and industrial use-cases tend to prefer a certain set of trade-offs, and I prefer a different one.

But it's a fascinating topic, and something that I'm preparing to devote the next several years of my life to. And I can safely say that a meteorite will more likely destroy Manhattan than will any of my computer science research be of widespread relevance to industry.

So, no, I totally disagree with everything you have said.




Guidelines | FAQ | Lists | API | Security | Legal | Apply to YC | Contact

Search: