[ The Types Forum, http://lists.seas.upenn.edu/mailman/listinfo/types-list ]
On 04/23/2013 02:52 AM, Mark Janssen wrote: > What machines do you use, where a C compiler fills in the gaps of your > source code? Quantum computers? Well, the C standard does not fully define the meaning of all C programs, e.g. when a program divides by zero. The actual program output may depend on the compiler options. The machine code is usually strictly defined, so in a sense the C compiler fills in gaps. The LLVM people have an interesting series of blog posts on this: http://blog.llvm.org/2011/05/what-every-c-programmer-should-know.html . In an attempt to better define declarative vs. imperative, or specification vs. implementation, it may be valuable to distinguish these categories of specification: 1. Functional specification 2. Asymptotic running time 3a. Asymptotic memory use 3b. Memory use up to a factor 2 4. Register use and instruction selection This list is by no means complete. Categories 2,3a are typically upper bounds: if the compiler can optimize stack usage from O(n) to O(1) by eliminating tail calls, that's fine but optional; the compiler does, in fact, compile according to specification. Furthermore, category 1 is typically a lower bound: the compiler may make undefined behavior defined. In my view, programs in these languages are specifications of these categories: ASP/SAT: 1 Prolog: 1, 2 Haskell: 1, 2, 3a Java: 1, 2, 3a C: 1, 2, 3b Assembly: 1, 2, 3, 3a, 4 Typically, the more "declarative" languages specify less categories. Apart from this numeric "axis", it may be interesting to regard the connection between how programs in a language correspond to the specification. For instance, programs in C explicitly have to free heap memory. In Java, objects are freed when they can no longer be reached from the stack. In Haskell, I guess thunks outside of global variables are freed when they can no longer be reached from the active thunk, but it is harder to make a mental model of this. One could thus argue that programs in "declarative" languages correspond closely to the induced functional spec, but loosely to the induced extrafunctional spec. Reversely, programs in "imperative" languages correspond closely to the extrafunctional spec, but more loosely to the functional spec. Cheers, Bram
