This language is small enough to write on a single piece of paper
Check, Clojure is one of the most concise language out there. I use it for hand writing code or when coding on my phone, because its so short.
fully contains all of its abstractions
Yup. In fact, you need to change your mindset, you don't write instructions in Clojure, you search for the functions that do what you want and arrange them in the order you need. Think micro-library.
has focused notation for specific instruments
Lisps like Clojure are the kings of DSLs. This is literally their bread and butter.
and permits debugging any part of a program by cutting any contiguous subprogram out and turning that fragment into its own live environment.
Yes, that's what the REPL lets you do. Load any subset of the program into a live running environment.
I'd write a program first on a prototyping platform which is so lightweight that nearly any prototype program will run, and I'd use that to write out the entire first draft of my program.
This is the idea behind dynamic programming which was invented by Lisp. Clojure will run almost any code, correct or not, no question asked. It does not put constrain on you, though it highly suggests the use of safe tools over unsage ones, it lets you cut yourself if you want too.
Then, I'd incrementally move pieces of my program transparently onto a more rigorously-precise framework which is more restrictive about types but makes it easier to compose modules and let them stay composed.
This is my ideal too. There's not yet the golden graal for this, but Clojure is currently focused on this very last part. Composing modules is actually pretty trivial, because it supports performant immutable datastructures as first class, open polymorphism, defaults to functionally pure constructs and wraps all state in safe managed containers.
Now as for correctness checks, it has optional types, but the implementation is a work-in-progress, and is stagnating a bit. Optional generative tests is the current strategy being explored, as well as highly powerful runtime checks. Still in alpha though. Static analysis is also being worked on, though soundness is not a target, also in alpha at this point.
If its any consolation though, the only two studies I could find about defect rates relating to programming language choice showed that Clojure does as well as Hakell. Which means it had some of the lowest defect rates of the languages tested, averaging a tad behind Haskell, and doing better then Scala and F#. Obviously besting Java, C++, Python, Ruby, C#, Go, etc. It was an outlier in that sense, as it was the only non staticly typed check language to do so well.