Ada does this. It's a nice safety rope but it can also get quite messy. Velocity equals acceleration times time? Nope, not without converting everything to a common base type. It is nice to know that you cannot mix different types by accident, but it also means you cannot mix them intentionally without writing more code.

Now I want to see a language that associates units with variables and intelligently checks that they remain valid throughout statements

And if you don't mind that it will probably your compile times and might have issues with compilers where certain types don't exist, you can use black template magic to get around ifdefs and having to know the different platforms and type sizes in advance.

Essentially you simply stuff all signed, unsigned and floating point types into a type list and let the template recursively go through this list until it finds one with the requested sizeof. Though this is only going to be of any help if a) you can't use the (c)stdint header and b) really don't want to worry about all the potential platforms. It's also going to be messy on exotic machines, where one "byte" can be more than 8bit.

 
template<bool condition, class A, class B> struct SelectT { typedef A Type; };
template<class A, class B> struct SelectT<false, A, B> { typedef B Type; };
 
struct NullType;
 
template<typename A = NullType, typename B = NullType, typename C = NullType,
typename D = NullType, typename E = NullType, typename F = NullType>
struct TypeList
{
typedef A Head;
typedef TypeList<B,C,D,E,F> Tail;
};
 
template<size_t size, typename list>
struct TypeOfSize
{
typedef typename SelectT
< sizeof(typename list::Head)==size,
 typename list::Head,
 typename TypeOfSize<size, typename list::Tail>::type
>::Type type;
};
 
template<size_t size> struct TypeOfSize<size, TypeList<> > { typedef NullType type; };
 
 
 
typedef TypeList<char, short, int, long, long long> SignedType;
typedef TypeList<unsigned char, unsigned short, unsigned int, unsigned long, unsigned long long> UnsignedType;
typedef TypeList<float, double, long double> FloatingType;
 
typedef TypeOfSize<1, SignedType>::type int8;
typedef TypeOfSize<2, SignedType>::type int16;
typedef TypeOfSize<4, SignedType>::type int32;
typedef TypeOfSize<8, SignedType>::type int64;
 
typedef TypeOfSize<1, UnsignedType>::type uint8;
typedef TypeOfSize<2, UnsignedType>::type uint16;
typedef TypeOfSize<4, UnsignedType>::type uint32;
typedef TypeOfSize<8, UnsignedType>::type uint64;
 
typedef TypeOfSize<1, FloatingType>::type float8;
typedef TypeOfSize<2, FloatingType>::type float16;
typedef TypeOfSize<4, FloatingType>::type float32;
typedef TypeOfSize<8, FloatingType>::type float64;

Ada does this. It's a nice safety rope but it can also get quite messy. Velocity equals acceleration times time? Nope, not without converting everything to a common base type. It is nice to know that you cannot mix different types by accident, but it also means you cannot mix them intentionally without writing more code.

Now I want to see a language that associates units with variables and intelligently checks that they remain valid throughout statements

As others have said, its possible to put together a pretty good system in C++ using templates, but some languages do have this kind of notion built in. Haskell and, I think, F# are two examples. I believe its called type annotation or somesuch.

Now, perhaps unfortunately, typedefs aren't strong

Ada does this. It's a nice safety rope but it can also get quite messy. Velocity equals acceleration times time? Nope, not without converting everything to a common base type. It is nice to know that you cannot mix different types by accident, but it also means you cannot mix them intentionally without writing more code.

Yeah, it does take effort to define the proper relationships, and it can grow into a sort of combinatorial problem. The approach would be to overload operators and/or create classes that represent various units. AFAIK, this is basically what the C++ template libraries do, except that they use template magic to generate the code, perhaps type traits as well in their implementation.

Its a mixed bag whether strong or weak typedefs are preferable, personally I think it would have been nice to have both options: typedef as strong, typealias as weak. C/C++ typedefs are weak mostly because C's notion of type equality is rooted in its physical properties (size and format), rather than its logical ones (its intent). That's a perfectly reasonable choice for a systems language, but its unfortunate that C++ didn't introduce a way to make a new strong type other than classes.