I think we should strive for strong type systems with a lot of type inference. I especially like Typescript for that.

Type systems are very useful to establish the semantics of your operations. For example `int + int` is not the same operation as `string + string`, and definitely not the same as `int + string` (which does not exist in most languages). You could call `+` an addition, but addition only exists for numbers, for strings it is a concatenation.

Is `int + string` the same as `string + int` ? (commutativity)

Is `int + int + string` the same as `(int + int) + string` or `int + (int + string)`? In that case, what does `int + string` returns? (associativity)

Now consider this code:

  def foo(a, b):
    return a + b

vs

  function foo(a: int, b: string) {
    return a + b
  }

In the second case, your function obviously seems wrong.

Finally, in math an object does not "have a type" but "belongs to a set/class". For example, "1" is an integer, an odd number, a real, a complex, a scalar, a rank 1 tensor, etc... Saying that "1" is only an integer is incorrect, but that's what most programming language do.

I've tried to design a language where "typeof variable == type" does not exist but instead you have "variable isof type" running the type checking code, example:

  class user(v: struct {
    name: string,
    logged_in: bool
  })

  class logged_user(u: user) check
    # this code is evaluated when 'isof' is called
    u.logged_in = true
  end

  class allowed_user(u: user) check
    # =>, <=> operators are logical connectors
    # A => B is true if A and B are true or A is false
    # A <=> B is true if A and B are both true
    u isof logged_in <=> u.name in ['admin', 'root']
  end

  let alice = { name: 'alice', logged_in: false }
  assert alice isof user = true
  assert alice isof logged_user = false
  assert alice isof allowed_user = false

  let bob = { name: 'bob', logged_in: true }
  assert bob isof user = true
  assert bob isof logged_user = true
  assert bob isof allowed_user = false

But lazyness got the best of me and I only implemented the parser :(