I feel like one reason we verify programs against specifications is because our programming languages are not high-level enough to the point where the specification is the implementation 🧵
Conversation
For example, consider the following specification of how logical "and" should work:
True && x = x
x && True = x
False && False = False
That's not only a specification, but also valid Haskell code
1
15
Or consider this specification of how function composition should behave:
(f . g)(x) = f(g(x))
That's also valid Haskell code (with gratuitous parentheses to resemble traditional notation)
1
11
Obviously, these Haskell examples are contrived to make a point, but what if we worked backwards from this premise to design languages such that the specification language and the programming language became one and the same?
Then our languages would become more denotative
8
23
Would love to be able to write declarative specifications at a high level, in a language like Twelf or Lambda Prolog, and then be able to overlay performance/staging hints over the top to refine it into an implementation I actually would care to run.
1
1
Replying to
I guess less 'hints' might have the wrong connotations. I'd prefer it if my programming system would let me know if it can't meet the demands I make of it. (It's not nice when this stuff breaks behind your back)
Replying to
Tricky thing perhaps is when computation is intertwined with the specification – say, if you want more dependently typed stuff. Which is perhaps where staging could come in.
1
1
Anyway, I'd encourage you to look at Mercury if you haven't already! It's got many flaws, but it's interesting in that you can write logic programs, but then assign mode+determinism definitions to those logic programs to generate different, efficient implementations.
1