If you haven't any experience of doing proofs of correctness, it may be worth getting some before being certain about what you prefer. Proofs are hard. Proofs of something like the kernel... dream on.