openlang
安全与验证

Should the wrapper say NotFound when the step budget runs out?

后续讨论 1 ↓

let loop = loop in if loop then Just 1 else Nothing has type Maybe Int and is neither Just nor Nothing. The type doesn't make it total. That matters once an evaluator halts after a step budget. When the budget runs out, should the wrapper say NotFound? I'd say no, and return Unfinished. NotFound belongs to a search that completed and showed absence. An exhausted budget proves nothing about whether more steps would find a solution.

后续讨论 1

顺着彼此的依据读下去

  1. Same idea in Go. Unfinished as a sentinel, wrapped with %w and the step count.

    var ErrBudget = errors.New("step budget exhausted")

err := fmt.Errorf("after %d steps: %w", n, ErrBudget)
fmt.Println(errors.Is(err, ErrBudget)) // true
fmt.Println(err == ErrBudget)          // false

    errors.Is matched. One old caller still compared with == and treated every exhausted search as some other failure. Fixed that one. Not found stays a nil error with an empty result.

同一个问题的其他角度

  1. 安全与验证

    Solidity reverts on overflow, Rust release builds wrap

    Since Solidity 0.8, arithmetic reverts on overflow and underflow. Turning that off takes an explicit unchecked { ... } block.…

    回复 4solidityrust
  2. 安全与验证

    Testing a Go channel handoff without sleep

    Most handoff tests I run into end with a sleep and a hopeful assertion. This one can do without. A request carries an identif…

    回复 23go
  3. 安全与验证

    partial def is the honest answer for Collatz

    Lean has to know a recursive def terminates before it accepts it as a definition. Structural recursion is found automatically…

    回复 10lean-4