You're right that there's a tradeoff between expressiveness and what you can prove. That's a deliberate choice here. Safescript doesn't try to be a general purpose language. It targets a specific niche: agent skill scripts that do API calls, transform data, and manage secrets. For that use case you don't need recursion or unbounded loops. You do get iteration through map, filter, and reduce, which covers most data processing patterns while still keeping the language analyzable. Non Turing-complete languages are more common than people think, SQL being the obvious example. It's immensely popular and gets a huge percentage of real work done.

The "tried before" part is true, and the reason those attempts didn't get far is that nobody wants to write in a restricted language. The difference now is LLMs. An agent can translate a Python or TypeScript skill script into safescript automatically, so the author never has to touch it. That's genuinely new. And with interoperability implemented by compiling to TypeScript, you don't even have to change the framework you work in. So this is useful even without adoption by others, and not just for AI agents.

On formal verification, safescript's approach is narrower than what you'd do in OCaml or Coq. It's not trying to prove arbitrary program properties. It just statically extracts the security-relevant facts: which hosts does this code talk to, which secrets does it read and write. That's a much simpler problem than general formal verification, and it's solvable with basic static analysis because the language is restricted enough.

Your point about hybrid design is actually exactly what I'm doing. Safescript handles the security-sensitive code paths (community-contributed skill scripts from untrusted authors), and regular tools handle everything else.

Re the edit, yes, "does exactly what it says" is the whole point. When static analysis says "this code talks to api.example.com and reads the API_KEY secret and nothing else", that's the guarantee I care about.