3 ms·

Further along: affine types, refinement types, formally verified preconditions/postconditions, maybe even dependent types.

• sterlind 2y ago
  Automatic theorem provers are stuck in AI winter. Pre/post-conditions and dependent types currently need too much handholding. Once the AI firms deign to release heuristic language models for proof discovery, we can have nice things like that.
  • alpine32 2y ago
    [dead]