Sometimes "academic" seems like a catch-all for stuff people don't like. Scheme has a strong academic history in its use and implementation, yet it seems to be described as "academic" only when someone is unhappy with how minimalistic it is, which is the opposite issue described here.
I want a language that is small, clean, and can provide a lot of static guarantees. I know many people find static guarantees and unacceptable curtailment of their "programming freedom", but frankly I think it's the answer to many of the problems we face in software today. Small is another thing. E.g. Go and Scheme are small. C++ and Scala are large. You know what I mean..
Now, static typing is just one kind of static assertion[1] I'd like to have. Side effect isolation (i.e. language-enforced purity) would be another feature I'd like to see become common. For example, the D programming language has a "pure" keyword that lets you mark a function as side-effect free. (In Haskell, all function are pure by default, and you escape the confines of purity via monads.)
I'd like to do research into (inventing) other forms of static assertions. One thing that's been on my mind lately, has been static "complexity assertion" for programs. I don't know if this even possible, but it would be nice to be able to ascertain before running a program, certain time & space complexity bounds on it. This would perhaps require us to drop the programming language itself to some level "slightly below" Turing machines -- but this in itself could be achieved via a keyword like D's "pure" or something more elegant. (Note: my point is not that we're going to make the entire language non-Turing complete -- but rather that we'll have subsets of the language that are not, and this reduction of power would/could bring with it a greater possibility for statically asserting stuff.)
[1] FYI I made this term up. Let me know if there's something better that describes this.
I don't know about knowing what "space" a program will consume ahead of time, but I believe the halting problem[1] means there'd be no way of computing a time requirement.
A trivial example would be a programming language that did not allow any loops or explicit backward branches. You would be able to provide upper bounds on how many operations such programs can perform.
> if you limit yourself to a language or a sub-set of a language that is not Turing-complete, then you can make static assertions about things such as halting
There's already something that is non-Turing complete, but comes with a halting guarantee -- it's called total functional programming[1]. This paper (linked below) is actually what got me thinking about this whole thing. The author argues in it how functions in functional programming languages aren't really like mathematical functions, because they have the possibility to execute infinitely (never halt) and thus not have a proper return value. To mitigate that, he creates "total functional programming".
Total functions are guaranteed to have a return value (i.e. terminate eventually), but they could take very long to run. If we could actually have complexity bounds, or be able to determine a given function's complexity, that would be a great boon to software engineering (i.e. assuming they adopt it... which is a whole different matter).
The author also makes a very good point that most parts of your program are meant to terminate (i.e. the vast set of functions and algorithms that comprise you program). Only the top-level needs to be Turing-complete, the rest can at least be total.
I actually want to see if it's possible to push this concept further, to create a ring-like hierarchy of languages -- the lowest one being the weakest and the one we can extract the most static assertions out of, and so on. There's a language called Hume[2] that sounds like it accomplishes at least part of this goal, but I haven't really looked into it.
[1] http://www.jucs.org/jucs_10_7/total_functional_programming/j...
[2] https://en.wikipedia.org/wiki/Hume_%28programming_language%2...
This is not true. Nothing about monads, in themselves, allows you to write impure functions.
Further discussion on LtU: http://lambda-the-ultimate.org/node/2131
[1] https://code.google.com/p/virgil/ [2] http://compilers.cs.ucla.edu/virgil/overview.html
Maybe its not totally exactly what you meant, but it can do basic analysis for loops.
ATS [2] is my go-to language for static guarantees with C's efficiency. Not sure if it counts as small but the implementation is not big.
[1] https://github.com/adamgundry/inch [2] http://www.ats-lang.org
Not necessarily a bad thing, for web development, most of it's depth is an over-kill.