Lambda the Ultimate

As seen on the haXe list, Elm:

Elm is a type-safe functional language that compiles to HTML, CSS, and JavaScript. It is also my senior thesis.
My goal is to make web development easier and more pleasant, and I decided to start from scratch. I hope that we will someday think of HTML/CSS/JS the same way we currently think of assembly (i.e. not for people).
Elm's major distinguishing features are support for reactive programming and its focus on visual presentation. Elm is also call-by-value and strongly / statically typed with type inference, so those of you already familiar with Haskell or ML should be quite comfortable.
Elm is very much a work in progress, so more examples and language features are on the way!

Comes with an interactive visual editor.

Let's suppose I am designing a simple programming language (imperative, statically typed, C-inspired), trying to integrate into it various ideas I like and hoping to be able to combine them into something nice.

I think I can implement the language (e.g. write the compiler), but I want my language to have at least some theoretical backing — I want to know that the semantics are sound, according to some definition of soundness. I do not want to dig too hard into formal PL theory — I merely want to be able to convince myself that the design is sane.

• What is the proper way of describing the static/dynamic semantics, to be able to reason about them more or less formally?
• What kind of «soundness» should I aim for, and what is the minimal sane required level of it?
• What are the most important properties of the language/type system, looking from the theoretical perspective (from a 80/20 perspective — the greedy 80%)?
• How can I approach formalizing those properties, and what are the typical ways of proving them?

Sorry if these questions are a bit too broad — without dedicated PL design education it is unclear for me where should I start. I will appreciate greatly if someone can try to answer these in simple terms, if possible.