As a pupil of Dijkstra and seeing at least some rise in formal verification because of the modern tooling and as a follower of Lean (and Agda, Coq, Idris* etc), I hope it will be at least a strive to deliver parts of proofs in code verifiable form. More machine verifiable building blocks will lead to a bettering of everything.
Offtopic, but I am 17 too just like Hannah Cairo but nothing too groundbreaking till now I suppose and it absolutely brings me delight that I can talk to somebody who was a pupil of Dijkstra, I have heard a lot about dijkstra's algorithm's and I had forgotten about it and so I searched it right now, but the only thing I knew is that it is pretty popular algorithm. If I had to ask you kind sir, what would be the bigge…
Pursue what interests you and what fires up your passion, not what grown-ups tell you is “lucrative”, “prestigious”, “profitable” or somesuch.