And what is a spec other than a program in a programming language? How do you prove the code artifact matches the spec or state machine
Say "I want HN client for mobile", "must notify me about comments", you see it and you add "should support dark mode". Can you see how that is much less than anything in any programming language?