You should try out Ada. It is a programming language that has syntax a lot like Pascal (i.e. English keywords). It is a compiled language and can do all of the fun imperative language stuff. However, what is really interesting about it is its type system, which is extremely strong and strict.
Ada doesn't allow implicit conversions. Every conversion between two different types (unless one type is a subtype of another) requires an explicit cast. Here is an example:
declare
number_of_beans: Integer := 56;
percentage_eaten: Float := 78.0;
begin
number_of_beans := percentage_eaten; -- Will not compile (this is a comment)
number_of_beans := Integer(percentage_eaten);
end;
But where it really gets interesting is when you add constraints to types and create new types using other types. You can create incompatible types from existing types (think of it as making a typedef in C, except the typedef cannot be used with the original type), create subtypes of types (this acts more like a C typedef, except that you can add constraints, such as the range of values allowed, to the subtype), and even iterate over the range of values in a type. Here's an example:
declare
type Bean is new Integer;
type Pinto is new Bean;
subtype Black_Bean is Bean range -67 .. 67;
subtype Small_Bean is Bean range 0 .. 1;
bean1: Bean := 5455;
bean2: Pinto := bean1; -- Will not compile (incompatible types)
bean2: Black_Bean := bean1; -- Will compile, but will raise runtime exception because the value of bean1 is outside the range of the Black_Bean subtype
bean3: Small_Bean := 0;
begin
bean1 := bean3; -- Will compile; Small_Bean is a subtype of Bean
end;
There is a lot more to it (it is quite a large language), but this is some of the cool stuff. Basically, the focus is to encode more assumptions into the type system and force you to be explicit about more of the assumptions you are making about your program. This can make Ada slower to write than a language like C but it can result in more readable/less buggy programs.
Ada doesn't come with the memory safety guarantees that Rust does, but Ada is designed in such a way that it discourages you from dynamically allocating memory explicitly (e.g. you can pass incomplete types, such as arrays with an unknown length, into a function, and the language will take care of the allocation/dellocation for you without you having to worry about passing by reference or value). It also protects against dangling pointers by including some rules that make pointers (called access types in Ada; they are not used much) illegal to use at scope levels higher than where they are initialized, making dangling pointers hard to do.
There is also a subset of Ada, SPARK, that can be formally verified mostly automatically, with the programmer filling in pre/post-conditions and letting a solver prove them at compile-time. This can lead to programs that are proven not to have errors (of any kind) at runtime.
It's pretty cool. There is a little tutorial at https://learn.adacore.com/courses/intro-to-ada/index.html if you want to take a look. I also like this blog post (http://cowlark.com/2014-04-27-ada/index.html) about someone exploring the features of Ada in more detail.