ATS

So what about it? Is it the next big thing (for respectable programmers such as lisp was (and seems to still be) and C)?

>>29
I know the feeling, but it's impossible to prove the need for those programs. Any proof would contain the equivalent of a decidability proof for the program.

I guess that proof could be more sophisticated than the set of predetermined rules, but I think the way to go about that would be to change the rules, then write your program according to them. If you're interested, try reading up on Coq.