I'm not sold on the pseudocode approach, but I agree with the declarative aspect. Declarative specs have become central to my process and I've built this tool to support it:

https://github.com/spekk-ai/spekk-cli

Rather than writing exhaustive specs, I preserve only the intent and what must be true as discrete assertions. This preserves the leverage you get from LLMs - anything it can reliably infer does not need to be specified. It also (mostly) separates intent from code or architecture decisions, which keeps specs flexible.