Re:Translating math into code with examples in Java, Racket,...
by pron on Wednesday May 29, 2019 @12:28PM
(#20042209)
> but is not quite as expressive
It's as expressive.
> For example, Hoare Logic cant really deal with Higher-Order things.
1. It can. 2. It doesn't matter so much, as there are no higher order "things" but rather higher-order ways to describe things. For example, in mathematics higher-order systems can be described as either higher-order ODEs or equivalent first-order ODEs. In other words, "order" is a feature of the signifier, not the signified. For example, things that would be higher-order in Agda are first-order in TLA+ (and you don't need to go that far: formal set theories are usually first-order, yet you need higher-order typed logics to describe the same things).
> They do struggle with more "extensional" properties, such as function extensionality.
Well, that's because they're constructive. There are type-theory-based proof assistants that more easily support classical mathematics, like Lean.
It's as expressive.
> For example, Hoare Logic cant really deal with Higher-Order things.
1. It can. 2. It doesn't matter so much, as there are no higher order "things" but rather higher-order ways to describe things. For example, in mathematics higher-order systems can be described as either higher-order ODEs or equivalent first-order ODEs. In other words, "order" is a feature of the signifier, not the signified. For example, things that would be higher-order in Agda are first-order in TLA+ (and you don't need to go that far: formal set theories are usually first-order, yet you need higher-order typed logics to describe the same things).
> They do struggle with more "extensional" properties, such as function extensionality.
Well, that's because they're constructive. There are type-theory-based proof assistants that more easily support classical mathematics, like Lean.