> There are theoretical and practical advantages to the functional style:
> - Formal provability
This is bollocks. To prove things about your programs, you need a formal semantics for the language you're using.
How precisely does modularity, composability and ease of debugging improve from this module? Not at all. It may have benefits, sure. But to claim these as general attributes is just sophistry in my personal opinion.
---
@lmm
> In practice no practical language provides formal semantics for the entire language
Programming languages are mathematical objects and always have a formal semantics, regardless of whether someone has taken the trouble to write it down or not.
What I'm saying is - the formal semantics that most languages have preclude the existence of compound values. Without those, you can't define interesting functions, and thus you can't program in a functional style.
> Programming languages are mathematical objects and always have a formal semantics, regardless of whether someone has taken the trouble to write it down or not.
Not true for the usual plain-english meaning of "programming language". Plenty of things we call programming languages take a "the implementation is the spec" view, or simply can't be assigned any useful semantics in a way that's at all aligned with the defining characteristics of the language in question. Even in, say, Haskell, io explicitly lacks formal semantics.
> What I'm saying is - the formal semantics that most languages have preclude the existence of compound values. Without those, you can't define interesting functions, and thus you can't program in a functional style.
Python tuples are perfectly cromulent compound values. Python has a bunch of builtin classes for which the equality operators that are available in the language are all kind of useless, sure, but that's true in almost all languages.
And do you think the implementation isn't a mathematical object itself?
> or simply can't be assigned any useful semantics in a way that's at all aligned with the defining characteristics of the language in question.
This is a contradiction in terms. By definition a semantics is a mathematical descrpition of the meaning of a programming language, i.e., the behavior of its programs. Sometimes a semantics exposes significant differences between the mental model of programmers and what a programming language really is, but the solution is not to turn a blind eye to reality.
> Python tuples are perfectly cromulent compound values.
So long as they have object identities, they are not values. Values are merely represented in memory - they truly exist in the language's semantics.
Only if you're taking the Tengmark "mathematical universe" view. The implementation is not necessarily any more mathematical than, say, a table.
> This is a contradiction in terms. By definition a semantics is a mathematical descrpition of the meaning of a programming language, i.e., the behavior of its programs. Sometimes a semantics exposes significant differences between the mental model of programmers and what a programming language really is, but the solution is not to turn a blind eye to reality.
The meaning expressed in a language is some alignment of what the writer intended and what the reader understood. If different readers don't reach a shared understanding then there is no meaning. It would be desirable for our programs to always have meanings that aligned with their behaviour, but we shouldn't turn a blind eye to the fact that many programs don't.
> So long as they have object identities, they are not values. Values are merely represented in memory - they truly exist in the language's semantics.
Any practical programming language will give you some way to find the memory address of a particular value, so values that we usually consider as semantically identical are not actually indistinguishable in practice. We deal with this by only assigning semantics to a subset of the language that excludes those operations. Python without "is" may be more obviously a subset than, say, Haskell without unsafeCoerce, but both are subsets.
The meaning of a program is its behavior, period. If reality doesn't agree with your views, it's your fault, not reality's.
> Any practical programming language will give you some way to find the memory address of a particular value, so values that we usually consider as semantically identical are not actually indistinguishable in practice.
Standard ML doesn't give you any way to get the memory address of a particular value, so values that are semantically identical are actually indistinguishable in practice.
> We deal with this by only assigning semantics to a subset of the language that excludes those operations.
That doesn't make sense. Semantics is a property of the real programming language you are using, not the fictitious one you wish you were using.
That's not the usual meaning of, well, meaning.
> Standard ML doesn't give you any way to get the memory address of a particular value, so values that are semantically identical are actually indistinguishable in practice.
Just tried it to be sure:
fun address i = Unsafe.cast(ref i) : Int32.int ;;
val a = 4 :: nil ;;
val b = 4 :: nil ;;
address (a) ;;
address (b) ;;
address (a) ;;
val address = fn : 'a -> Int32.int
val a = [4] : int list
val b = [4] : int list
val it = ~175003712 : Int32.int
val it = ~174998232 : Int32.int
val it = ~175003712 : Int32.int