compiler engineer, programming language designer, proof automation specialist, researcher in computational logic