How to define the formal and informal semantics of an algorithm as accurately as possible? I am currently researching ways to define the semantics of programs for some ideas I have for a new programming language. Most ways to define semantics involve mapping the programming language syntax representation of a program to some semantic specification. I dislike this approach, because the syntax restricts what semantics you are able to express and it often results in the under and over specification of the semantics.

Instead of thinking of a programming language in terms of syntax constructs and their corresponding semantics, I want to focus on semantics first, syntax, although important to be able to best read and write programs and ultimately necessary to formulate the semantics, is of lesser importance. But in order to do so, I need a language that is capable of defining the semantics as accurately as possible. This semantic language should not be a programming language by itself, because its main purpose is defining semantics accurately, not computations. So I think most formal semantic specifications do not comply to these requirements, because they focus on extracting semantics out of existing programs instead of defining them as accurately as possible in the first place. Therefore I would like to ask the following question:


  "Are there any languages or methods that focus mainly on expressing formal and
  informal semantics of an algorithm as accurately as possible?"


During my research I was reading "Formal Syntax and Semantics of Programming Languages" by Kenneth Slonneger which include some chapters about the different ways to define the semantics for a programming language. In chapter 11 (Axiomatic Semantics), page 397, he states that "Extensive literature has dealt with the difficult problem of accurate specifications of algorithms.". But I have a difficult time finding literature that is specific about "accurate specifications of algorithms". Therefore my second question is as follows:


  "Do you know about any literature that specificly talks about how to
  define accurate specifications of algorithms?"


Edit: To make more clear what I mean by "expressing semantics of an algorithm as accurately as possible" I will give an example. If with axiomatic semantics the following pre and post conditions were given:

pre  = m &gt;= 0 and n &gt;= 0
post = minimum &lt;= m and minimum &lt;= n and minimum &gt;= 0


Then the following function would comply:

minimum m n = 0


But this does not capture the intent the person writing the specification had.


  "Do you know of methods that could capture this intent more accurately?"
I don't know how you can define the informal semantics as accurately as possibly, but there does exist machinery for defining semantics that is purely, well, semantic. 

Your semantics could be based on mathematical functions, relations, or domains. Indeed, the style of semantics known as Denotational Semantics builds upon these (and other) semantic notions by mapping the syntax in a compositional fashion to some semantic domain. 

If you don't want syntax for your programming language, then start directly with the semantic domains (for example, those from Domain Theory). In this setting, each type in your programming language will be represented by a semantic domain and algorithms will then be functions from one type to another.