C/C++ interop and OS interactions are separate issues mostly orthogonal to type systems.

Teaching would probably start without using the type annotations for simplicity. Let the students get something working first with basic dynamic code. Then teach the type annotations and reasons for using them in more advanced courses.

    sub add(\number1, \number2) { number1 + number2 }

    say add(1, 2) # 3

    say add(0.1, 0.2) == 0.3 # True

    say add('0.1', '0.2') == '0.3' # True

    say add('foo', 'bar') == 'waldo'

----

The student moves on to a more advanced course...

----

Type annotations are introduced:

    sub add(Numeric \number1,
            Numeric \number2) { number1 + number2 }

    say add(1, 2) # 3

    say add('foo', 'bar') == 'waldo'

So, reason 1 for using types: get type-checking that catches errors at compile-time.

You can use native types for closer-to-the-metal speed (compact representations, no automatic overflow checking, etc.):

    sub add(num64 \number1,
            num64 \number2) { number1 + number2 }

A third reason for explicit types is to take advantage of C interop:

    use NativeCall;
    sub add(int32, int32) returns int32 is native("calculator") { * }

    say add(1,2)

And so on.

At one point you do have to make a decision though. If you come from a static type system, the compiler rejects programs if it can't proof their type correctness. Dynamic languages that introduce statics types typically do it the other way 'round: in case of doubt, allow the program at compile time, and possibly throw a type exception at run time.

You can try to make separate decisions in separate scopes, but then you have problems at the boundaries between such regions.

The point I'm trying to make is that gradual typing comes with its own complexity, both on the implementation side and through cognitive load for the programmer.

It doesn't have to be any harder than a language with a JIT VM. See Strongtalk and Dart.

At one point you do have to make a decision though. If you come from a static type system, the compiler rejects programs if it can't proof their type correctness. Dynamic languages that introduce statics types typically do it the other way 'round: in case of doubt, allow the program at compile time, and possibly throw a type exception at run time.

Also wrong. See Strongtalk and Dart. If you wanted to, you could make a variant of either system not compile your app without every type specified.

Like tightening the bolts. This is a really interesting idea. I could also envision a utility wizard that you could run on a piece of code that could help guide you through making things more specific by asking you questions about the code. Are tools like this out there already? Like if you've defined a string and you run the utility it would ask: “Is this variable a number? Yes/No.” and then change to ensure it's a number in your source?

EDIT: Found one for you:

http://mypy-lang.org/

This is the Perl 6 view. See "Getting beyond static vs. dynamic" http://www.jnthn.net/papers/2015-fosdem-static-dynamic.pdf

In Perl 6:

> 1. A value.

    sub (\var) { say var }

    sub (Numeric \var) { say var }

    sub (Num \var) { say var }

    sub (Num \var where 0.0 .. 100.0) { say var }

    sub (num \var where 0.0 .. 100.0) { say var }

Did they take it as far as Perl 6 per the above?