3. Lisp is nice, but the implementations have issues. I'm mostly satisfied with SBCL at the moment, but I keep writing utility functions to get around the warts in the language. Languages seem to be an instance of the "all X sucks - some just sucks less" pattern.
4. I think providing explicit support for state machines would be a Good Thing even without the visualizer.
5. Something that lets you look at an expression as you step through evaluation and substitution would be useful. Macroexpand does this at compile-time, but I want something similar at runtime for parts of the expression that aren't macros. I suspect something like this exists, but I haven't seen it yet. Slime's disassemble takes the name of a function and displays the corresponding assembly code in a buffer.
I agree that it's not practical at this point to try to completely prove the correctness of programs; I think it's more useful to prove specific aspects of a program as an alternative or supplement to tests. It's also useful to make assumptions about things you can't prove in the mathematical sense but can rely on when writing or running a program.
What's next? I've been meaning to download and try out Qi, a language that builds on top of Common Lisp and has a type system based on sequent calculus. It looks like Qi allows users to start with fairly general types and narrow them down as the program develops.
I didn't enjoy OCaml when I spent a couple days trying to learn it. The restrictions of the type system were frustrating, though I did get the feeling that it's a much better way to keep people from breaking stuff in a "software engineering" situation than using Blub.
1. A[i] and Ai (that should be subscript) seem pretty similar to me, but I like Ai more, it just seems cleaner. In C# we can write A[i,j,k] for multidimensional indexers, but tensor script seems cleaner still. Again, I think this really depends on background -- someone who actually deals with tensors might find my proposal more attractive. I'm just driven up the wall when I have to write A[i][j][k]. It's so wasteful.
2. I'm not sure if it would be harder to navigate with a keyboard -- it seems like something that you'd have to build first and get used to. The idea of implementing these things as macros which compile down to regular syntax really appeals to me, in fact it's what I had in mind. (C++ has awkward features to do this in the STL with templates, and numerous TopCoders include C macros to expand summation, product, or accumulator functions. If they're useful in the heat of the moment, why not in regular usage?)
3. Nice. Thanks. At some point I'll have to take on another big product in LISP, I haven't really touched it since I went into scientific computing, and I think my opinion of it was colored by the bare-bones Scheme I was using.
4. "Detecting... would be hard" -- it doesn't have to be perfect. I mean, if it was perfect, implicitly it would mean 'graphically model arbitrary code'. I'm thinking there are a collection of schemes which might find maybe 80% of what people would call state machines which aren't so bad. Maybe 80% isn't satisfying, but it's a start. Like bug catching codes in compilers, it won't work all of the time, but maybe it's not necessary.
It might be easier to reach at it via making a creation and display layer though, you're right.
5. It seems like macroexpand is basically what I'm looking for -- at least it's powerful enough to do what I want it to do without too much pain. I'm unfamiliar with Slime's disassemble command, and the first Google page was unhelpful...
As for language support for provably correct programs, they sound interesting to me, too. They should definitely not encompass the whole language though. To be honest I'm not really sure that the mathematics is where it needs to be. So many proofs rely on obvious things, not 'obvious' in the naive sense, but actually obvious, and it seems like such a pain to program these in that provably correct systems are impossible to use, at the moment. Yet, Doron Zeilberger seems to think otherwise.
I don't know how to escape the problem of infinite regress, or, set differently, Godel's incompleteness theorem. Any sufficiently powerful proving system we have is unable to prove it's own consistency, so, as someone who is admittedly unfamiliar with this territory, I don't see where the starting point is for so called provably correct programs.
What would you guess the next step in the right direction is?