I rather enjoy the programming style one has to program in when developing in Coq. It’s a fascinating idea: write a specification, then refine it until finished. There’s an addictive, puzzle-like nature to it that i adore. I read on “test-driven development” and i’m like, but the system can help you so much more if you have full specs and not just tests!
Are there any similar systems for more popular languages? That is, would it be possible to use a specification language for something like Python, C, Java, Haskell, etc, and then have some way of using said spec as a guide to writing programs?
PS: Extraction does not count!
(i’m not married to the idea of using tactics; i think what they have working in Agda would be fine, too, in something other than a proof assistant ofc)