4 ms·

I meant 1). Drawing by example from TypeScript and Java nullness checkers, certain programming idioms are fine in practice and programmers can reason about the

by wffurr 5y ago

I 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.

sanxiyn 5y ago
RefinedC doesn't have that problem then. That's what is meant by "foundational" in the title.
- wffurr 5y ago
  OK. That wasn't clear at all from the description of "foundational" in the article, which instead discussed the "trusted computing base" of the provers.