> the catch is that it isn't doing classical (logical) type-checking, but, instead, it "type-checks" by inspecting with random samples. So it's almost nothing

> the catch is that it isn't doing classical (logical) type-checking, but, instead, it "type-checks" by inspecting with random samples. So it's almost nothing like Idris, which is geared towards formal verification. All of these unsound type systems make development and refactoring easier, but you don't really know what type checks are being done at a lower level. TS* has (had) an untrusted type for input from potentially hostile adversaries. I would have preferred to do high-assurance client side code development in that, but it's no longer maintained.