> for loops and arrays are implemented are broken? Well actually they should rarely be used A great motivation: it's always better to write half-assed implemen

> for loops and arrays are implemented are broken? Well actually they should rarely be used A great motivation: it's always better to write half-assed implementations of rarely used features because they are rarely used. > You do not need a complete language like F# and C++ to write contracts Agreed. You need a small verifiable DSL, not an entire new language. > Once again the type system doesn't need to be perfect That's the spirit when designing a language! > it amazing to see the progression Well... yeah, if you started with the goal of executing without crashing it can only improve over time.