4 ms·

Your last point is what I was trying to get at — eg, reasoning just about your math expressions. https://herbie.uwplse.org/ https://herbie.uwplse.org/ I think

Your last point is what I was trying to get at — eg, reasoning just about your math expressions. https://herbie.uwplse.org/ https://herbie.uwplse.org/ I think that FM (beyond basic typing) is best used sparingly to address particularly sensitive cases — eg, floating point stability in modeling. But our discussion usually doesn’t include incremental or partial usage, unfortunately.

rocqua 1y ago
I've been looking at incremental / partial formal verification based on 'assert'-like statements. Kani for rust has an interface close to what I imagine. But I'd like to use deductive verification (something like hoare / seperation logic) instead. This means the developer gets to decide what is important enough to try to assert. It's likely the developer will need to add sub-lemma's to get the assert to be proven, and I suspect some of these will need to be in the form of 'assumptions / requirements' at the start of a function, which then need to be confirmed at all call-sites. A big downside here is that some things you'd like to prove often don't fit into boolean expressions in the underlying language. For example, universal / existential quantifiers aren't available (but are implicit in the formal prover, so can be hacked into). You also don't have predicates for 'this address has been allocated / initialized' nor any other predicates that let you say a value is constant. Similarly, there are no temporal quantifiers available. I'm hoping that the above is not too limiting in practice. The fact that developers already user 'assert' statements does suggest that normal boolean expressions are already valuable.
naasking 1y ago
> Your last point is what I was trying to get at — eg, reasoning just about your math expressions. I think it's borderline criminal that programming languages haven't added units of measure to their type systems yet, and then required every numerical type to be associated with a unit. We've known how to do this for decades now. All numerical code has latent units: either a specific unit, or polymorphic over the unit (like scalar transforms). Even memory copies and moves operate on byte units.
- rocqua 1y ago
  C++29 is considering adding units. Currently, apparently, available in this library: https://mpusz.github.io/mp-units/HEAD/ https://mpusz.github.io/mp-units/HEAD/
  - naasking 1y ago
    Great news if true, but I'm not holding my breath. Just adding units support doesn't quite go far enough, but C++'s backwards compatibility prevents it from enforcing the stronger requirement I mentioned.

rocqua 1y ago

I've been looking at incremental / partial formal verification based on 'assert'-like statements. Kani for rust has an interface close to what I imagine. But I'd like to use deductive verification (something like hoare / seperation logic) instead. This means the developer gets to decide what is important enough to try to assert. It's likely the developer will need to add sub-lemma's to get the assert to be proven, and I suspect some of these will need to be in the form of 'assumptions / requirements' at the start of a function, which then need to be confirmed at all call-sites. A big downside here is that some things you'd like to prove often don't fit into boolean expressions in the underlying language. For example, universal / existential quantifiers aren't available (but are implicit in the formal prover, so can be hacked into). You also don't have predicates for 'this address has been allocated / initialized' nor any other predicates that let you say a value is constant. Similarly, there are no temporal quantifiers available. I'm hoping that the above is not too limiting in practice. The fact that developers already user 'assert' statements does suggest that normal boolean expressions are already valuable.

naasking 1y ago

> Your last point is what I was trying to get at — eg, reasoning just about your math expressions. I think it's borderline criminal that programming languages haven't added units of measure to their type systems yet, and then required every numerical type to be associated with a unit. We've known how to do this for decades now. All numerical code has latent units: either a specific unit, or polymorphic over the unit (like scalar transforms). Even memory copies and moves operate on byte units.

rocqua 1y ago
C++29 is considering adding units. Currently, apparently, available in this library: https://mpusz.github.io/mp-units/HEAD/ https://mpusz.github.io/mp-units/HEAD/
- naasking 1y ago
  Great news if true, but I'm not holding my breath. Just adding units support doesn't quite go far enough, but C++'s backwards compatibility prevents it from enforcing the stronger requirement I mentioned.