abab9579 (Oct 27 2022 at 09:14): abab9579 (Oct 27 2022 at 09:14):I have been playing with coq for some time, and loving it so far. Currently, I am a regular math major who is going to graduate school next year. Is there a way to perform such computerized proofs as part of a career? I am curious if such career path exists. Also, what is the requirement for the career, if it exists? Any answers would be greatly appreciated!
Li-yao (Oct 27 2022 at 09:47):The most common might be an academic career. You can get an idea of what people are doing from academic conferences and workshops like POPL, CoqPL, or CPP which regularly attracts industrial users as well. There is also this list of companies that use formal methods https://github.com/ligurio/practical-fm For Coq specifically, Galois, Bedrock Systems, SiFive, and Huawei are some notable ones that come to mind.
Michael Soegtrop (Oct 27 2022 at 10:18):There is quite some interest by the industry as well I would say. But currently the common path to get into this is likely to do a Ph.D. in the field. In a few years, when the ground is further paved, it might not be uncommon to get into this with a master in the area.
Karl Palmskog (Oct 27 2022 at 10:49):Some quick additional examples of Coq use in industry:
Karl Palmskog (Oct 27 2022 at 10:50):generally, there are quite a few blockchain-related companies using proof assistants in some form
abab9579 (Oct 27 2022 at 23:17):Thank you so much! I want to pursue academic path, so I guess I would be able to follow the PL side. Are there more type theoretic / mathematical side as well? Personally I would not mind switching to e.g. Lean to do this.
Théo Zimmermann (Oct 28 2022 at 07:55):Yes, PL is a very represented field using Coq, but mechanized proofs are represented in more and more fields. If you have a specific field you are interested in, you can probably find people using proof assistants (or considering it) for it. Lean has a strong "classic math" community, but you can also find people doing "classic math" in Coq (e.g., math-comp analysis). If by theory you also mean logic, then there are plenty of opportunities in the Coq community as well.
Karl Palmskog (Oct 28 2022 at 09:02):one of few areas where there is industrial interest in mechanized pure math is when it's related to cryptography. For other pure math, I'd say there are almost only academic jobs (and research institutes)
abab9579 (Oct 28 2022 at 11:02):Thank you again. I am mainly interested in pursuing academic jobs, and wanted to know which fields I could go for. I guess learning Lean could be a better idea.
Karl Palmskog (Oct 28 2022 at 13:07):At least currently, the research grant money available for pure math formalization is small compared to the grant money for applied formalization. Probably something to keep in mind. Papers that only "formalize math concept X" are getting harder to get accepted by the hour.
abab9579 (Oct 28 2022 at 13:55):I know, but coming from math major I feel barrier for "applied formalization" might be as high for me. I expect reading industry demands would be crucial for both the research and industry work, and I am terrible at this skill.
For now, I am gauging the computerized math (either classical or intuitionistic / logic) path against pursuing pure math as it is, and that path would be challenging as well. Indeed, I guess some subfields of pure math would be out there where people just began pioneering. Not seeing any right now, though.
Yosuke Ito (Oct 29 2022 at 02:48):Just my own feeling, but it seems that Japan is far less developed in formal verification in the industrial areas.
Last updated: May 31 2023 at 02:31 UTC