The problem: In order to prove a specific goal you need all information derivable from a term; and with juggling around only local information, I cannot convince myself I could arrive at a typing system which would prove specific goals given all information derivable in the term.
I am not sure how general this problem actually is. The closest typing system I could look at is Haskell, and there are no results on this problem. I gather they patched a system together which usually works.
The language I am now developing looks naked though. It'll become an experiment in how to write untyped algebraic specifications.
Too slow for anything useful probably but a nice experiment.
After the new language is developed enough, I'll start a new blog. Goodbye Hi.
