Lean is a modern, functional, dependently-typed programming language that allows both to write efficient code (with a foreign function interface to C), but at the same time can serve as a proof assistant, via the proofs-are-programs principle.
We can start with the functional programming, start with a toy arithmetic expression DSL and an interpreter. We could grow the language. We could learn to use of monads and monad transformers to represents effects, look into the difference between first-order and higher-order representations of syntax and their benefits and drawbacks, try out well-typed and well-scoped syntax. Maybe along the way something that fits your personal interest comes up?
References: