[lmm]

Cardelli's definitions are extremely odd; if you take them literally then Python is type safe but Java is not.

In everyday language a downcast, even a checked one, is not a type-safe operation, and so to the extent that Go's limited type system makes it impractical to write programs without downcasts I'd say that Go is fundamentally type-unsafe.

[Joker_vD]

Well, it's a matter of taste, I guess. In my opinion any downcast that reliably distinguishes between valid and invalid values is type-safe. The behaviour of

    defer func() {
        if e := recover(); e != nil {
            fmt.Printf("not a string %v\n", e)
        }
    }()
    v := interface{}(5)
    u := v.(string)
    fmt.Println(u)

is well-defined: it will print "not a string", always.

[lmm]

By that logic there's no such thing as a non-type-safe language, because all programs have behaviour.

Normally one would say a checked downcast like that is not type-safe, because you can't reason locally about the type behaviour of the downcast based on knowing the type of v. You would have to know the value of v, which is a Turing-complete problem in the general case.