You might be interested in this study as a way of refining your interests and goals: http://loonwerks.com/publications/pdf/cofer2013fmics.pdf http://loonwerks.

You might be interested in this study as a way of refining your interests and goals: http://loonwerks.com/publications/pdf/cofer2013fmics.pdf http://loonwerks.com/publications/pdf/cofer2013fmics.pdf It's a big world out there; this has been an active area of research basically since Turing. Many of the "relationship between" questions you ask have their own conference or workshop series. > formal provability IMO the best way to start down this road is to just begin using some of the tools out there -- TLA+, Coq, whatever - and touch base with the community around your choice of tool (conferences, workshops, or even going back to school for a phd). The best way to learn about the strengths and limitations of current software practice is to sit down and churn out code, preferably with a strong mentor. The same is true for proof programming.