I want to do my vibe coding in a dependently typed language, so that at least I can tell what the inputs and outputs are. I say Idris is the future!

Or... I want to only write the tests. The implementation is... an implementation detail!