@mobileink @sophiago I was thinking about those "denotational and operational semantics" recently. I was wondering if perhaps Clojure's focus on powerful, literal data structures, helps transfer complexity from code to declarative data. The associativity of maps, for instance; they have both form and function - logic is built in and, because they're literal, the logic is explicit. So you can trade the complexity of function logic, which operates over data structures, with complexity in your data structure. It's a matter of where you want to store your complexity. A good example is a project.clj file - dense complexity, where the hierarchy of the computation is declared by the shape of the data structure. Also, reminds me of this tweet: https://twitter.com/fogus/status/454582953067438080

you really need static typing to develop denotational semantics for a program. i suppose you could write the semantics before writing the code (what Conal Elliot refers to as "denotational design) but it'd still be very difficult to know whether your code matches it

there seems to be some confusion here generally surrounding the difference between declarative PL design and actually encoding the semantics of a program

i think the best way to explain it in Clojure terms is that the specification you write for spec would be the operational semantics of your program (although it would be a bit nuts to make it as fine grained as you get handed to you by a strong static type system) and the "check" part verifies that your implementation matches it. this is the same as in Haskell's Quickcheck, except you don't have to write the spec: it's just the type signature. so both are operational semantics, whereas in a language like Haskell you can sometimes also reason with denotational semantics in the form of "static analysis," in other words when everything your implementation does is represented in the type signature (mostly when you don't need to encapsulate effects in monads and can instead write in an "applicative style").

hmm, I'm a bit of a static typing sceptic 🙂

I'm no expert on them and I don't really know Haskell, but I think I grok what you're saying.

yeah, i use both so not trying to evangelize for it

just saying, i think Clojure is pretty squarely in the domain of operational semantics and a bit informally at that

iow, you'd have a super rough time say...verifying a Clojure program is high assurance in a theorem prover like Coq or Agda. it it's even possible at all (probably not)

Couldn't you with spec?

I guess not at a "whole program" level

I just get the feeling that formally specifying all behaviors actually makes a program brittle, on the operations side. Seems that sometimes the power of a function resides in its not-necessarily-defined behavior.

spec doesn't offer anything remotely resembling denotational semantics. you can google Scott-Strachey semantics and take a look at what we're talking about

it's literally a way to encode the behavior of your program using formal logic, which is why you can use it as the basis for mathematical proofs

this means a semantic specification of a program that doesn't define all of its behavior is by definition...incorrect

I see

right, so it's quite a bit heavy-handed for anything i can imagine you're thinking about

enjoy 😄

Looks like wikipedia agrees with you: Perhaps the first formal incarnation of operational semantics was the use of the lambda calculus to define the semantics of LISP

i didn't even know that, but makes sense

an interesting bit of trivia is the idea of stream processing (and hence lazy evaluation) pretty much came from Peter Landin's attempt to develop an operational semantics for if-then-else statements in Algol-60 (which, of course, originally came from Lisp)

it makes sense if you think about it. that's how i explain lazy evaluation to beginners: in every language only one branch of an IFTE statement is ever evaluated

My intuition about the words "denotational" and "operational" want me to interpret them as "explicit" and "implicit." But reading their wiki pages, that doesn't appear to be case.

Yeah, they're both explicit by definition. But I would say in order to have a reasonable denotational semantics you need certain things about the program itself to be explicit (which as I mentioned, goes beyond even the strongest static typing...at least imo)

well, that last bit is pretty opinionated. i think many haskellers would call me out of it

🙂

I just upgraded from free to premium TODOist. AMA.

what's a good fitness band ?

@qqq SBTRKT, Boogarins

?

fitness band as in apple watch, microsoft band, jawbone, .... ?

is there a channel about videos of talks?

@dpsutton : I'd like that -- a place to discuss / share interesting talks.

yeah i'm at work and was wanting to put some on in the backgorund