Is trying to build my own proof assistant a sensible project? I have a Math background; I'm learning Haskell and Scheme, but I have no other experience with programming. I want to start and finish a project precisely in order to get into programming and theoretical computer science.