Yes, exactly. At first we wanted Ruby, but compiled. We started with something that was very, very similar to Ruby (except some dynamic aspects) but the type inference algorithm was very slow. So we made some sacrifices (like telling the compiler the types of Arrays and Hashes) and that made the compiler very fast. But at that point we diverged from Ruby because the syntax was starting to be different at places. Then because of how we deal with Nil we changed some of Ruby's semantics (like, Array#[] raises when out of bounds), so we can't say Crystal is a compiled Ruby: it's a totally different language. It just happens to have a pretty similar syntax and API to that of Ruby :-)
Could you comment a bit how the approach you took on Crystal differs from what's described in the OP? (... “Soft Typing” [1], introduced by Mike Fagan in his 1991 dissertation ...)
It's hard to say, the paper is really long and it's full of mathematical notation that is hard to digest and there are no examples to make it easier. Or, if they are, they are for a symbolic lambda calculus program.
The problem with this kind of papers is that they are for a hypothetic programming language based on lambda calculus. In Ruby we have objects, instance variables and blocks. We have inheritance and modules. It's hard to make a 1-1 mapping between the paper and the real language. This is why Matz said (if I remember correctly) that the algorithm would need to be adapted to an object oriented language like Ruby (so you can imagine, the paper doesn't even deal with objects, probably just functions!).
Before developing Crystal we read some papers, but all of them were pretty limited (they only dealt with primitive types like int and float). We had to think of a new algorithm that adapted well to all of the language features. And the algorithm is very specific to the language, which is something good because we can make it optimal, instead of for a general language.
It's hard to describe the algorithm in detail. We'll eventually do so in blog posts.