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!

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, Si-Five, and Huawei are some notable ones that come to mind.

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.

Some quick additional examples of Coq use in industry:

generally, there are quite a few blockchain-related companies using proof assistants in some form

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.

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.

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)

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.

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.

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.

Just my own feeling, but it seems that Japan is far less developed in formal verification in the industrial areas.

Last updated: Jan 29 2023 at 18:03 UTC