> don't think it's too far off though, since we can (and, as I argued, should) tease apart the data from the assertion, to get something like `let x = 3; assert(x > 2)`; and that's equivalent to `(lambda x: assert(x > 2))(3)`
Right, but even that is an unquantified proposition.
> If I try stretching my constructive-logic argument a bit, we could implement negation `¬A` as a function `A -> Void`
There's no need for constructive logic specifically (a test presumes that it runs in some bounded time, which means we're operating on finite domains). Tests can invert both their assertions and their result, so if they were existentially quantified they could also have been universally quantified.
Indeed, tests can express (though not effectively execute) an existential quantifier (∃xP(x)) over a finite domain (though not infinite ones):
for x in Domain {
if P(x) return true // test success
}
return false // test failure
And that can easily be turned into a universal quantifier through negation:
for x in Domain {
if !P(x) then return false
}
return true
This is the exact transformation as in (∀x : P(X)) ≣ (¬∃x : ¬P(x)); the internal predicate is negated and then the entire thing.
> but test suites rely on runtime execution, which is inherently untyped
Types are a syntactic concept and they are, therefore, a property of a language; a language can be typed or untyped (types serve as part of the rules for determining whether a string is in the language or not). There are several ways to describe execution, but usually it isn't described as a language, so it is no more typed or untyped as it is yellow or not yellow.
Right, but even that is an unquantified proposition.
> If I try stretching my constructive-logic argument a bit, we could implement negation `¬A` as a function `A -> Void`
There's no need for constructive logic specifically (a test presumes that it runs in some bounded time, which means we're operating on finite domains). Tests can invert both their assertions and their result, so if they were existentially quantified they could also have been universally quantified.
Indeed, tests can express (though not effectively execute) an existential quantifier (∃xP(x)) over a finite domain (though not infinite ones):
And that can easily be turned into a universal quantifier through negation: This is the exact transformation as in (∀x : P(X)) ≣ (¬∃x : ¬P(x)); the internal predicate is negated and then the entire thing.> but test suites rely on runtime execution, which is inherently untyped
Types are a syntactic concept and they are, therefore, a property of a language; a language can be typed or untyped (types serve as part of the rules for determining whether a string is in the language or not). There are several ways to describe execution, but usually it isn't described as a language, so it is no more typed or untyped as it is yellow or not yellow.