Interesting, but I'm not clear on how the "adequately justified" part would work. Wouldn't the second test accept this function?

(define (foo x y) (+ 4 (* x y)))

And thus not be "adequately justified"? You would have to try all possible arguments to make sure that no other function would fit the tests.

It would probably go over as well as Ada did.

Ian, the idea is to do something like what Jester does -- it has a library of mutations to apply to code, and if you survive all those mutations, then the code is "good enough". Examples include negating the test of an if statement or while statement, changing a zero to a one, and a few others. I just made up the idea of replacing + with * because it kept the example simple. I would also expect the language to allow programmers to define their own mutations for functions they've written.

Sean, the point isn't to make a commercially successful language. Commercially successful languages are rarely interesting. If such a project became as successful as Ada, I would count it as successful beyond my wildest dreams.

Hm. You know in Smalltalk debuggers there's a button you can press to create a nonexistent method that you had tried to call. How about a programming environment where that's the only way to create a function? It'd be less strict about forcing you to test, but feel less like a nanny making you jump through hoops, perhaps. Could this be generalized so you could only introduce IF statements, etc., by supplying examples?

I haven't used Epigram, but this reminds me of how its environment is said to expand code-in-progress based on types.

Darius: That Smalltalk feature is quite a bit like the Eclipse "Quick Fix" feature. It allows one to write code that doesn't compile (eg, by referencing a method that doesn't exist) and then hit C-1 to fix the issue by adding a method with an empty body. This style of development is how I write most of my code these days.

Regarding a compiler that proves that code is tested, it seems like the analysis has to be dynamic, which means it could get very expensive. I wonder what static analysis you would add to it to make it efficient (ie, detecting what tests can't possibly test a block of code and not bothering to run them).

Darius, I like the idea of making examples be part of the required syntax for an if statement. Unfortunately I'm not sure it would work well for such a small piece as an if statement -- unlike functions, if statements aren't usually designed to have a small surface area.

Richard, a simple way of reducing the runtime overhead would be to syntactically tie the tests to the code. Then it would be immediately obvious which tests need to be run to validate the code, since they're right there next to it. One way to think of it is as an extension of the idea of a method signature.

I'm reminded of the Guantanamo tool for Java. It deletes any code not covered by tests.