3 ms·
When you say "may not be provably safe", do you mean 1) it is safe but hard to prove, or 2) it is not safe? RefinedC is sound, so it can't handle 2. For 1, whil
by sanxiyn 5y ago
When you say "may not be provably safe", do you mean 1) it is safe but hard to prove, or 2) it is not safe? RefinedC is sound, so it can't handle 2. For 1, while it focuses on automation, it has an escape hatch with which you can use full prover, so it should be able to handle anything that is actually provable.
- wffurr 5y agoI meant 1). Drawing by example from TypeScript and Java nullness checkers, certain programming idioms are fine in practice and programmers can reason about them, but they're difficult to express in a provable way. Sometimes it's limitations in the tools; other times it's actually unsafe but safe in practice due to an invariant maintained elsewhere but not actually expressed in the code under consideration.