On Thu, May 9, 2024 at 9:17 AM Thomas Passin wrote:
> I always thought that formal verification (FV) of programs would be too
> hard and error prone beyond simple programs. Apparently I was wrong about
> that, and one reason is that FV should be applied above the program level -
> e.g., to
Darn, the title was supposed to say "*Formal* Verification ...".
On Thursday, May 9, 2024 at 10:17:01 AM UTC-4 Thomas Passin wrote:
> I always thought that formal verification (FV) of programs would be too
> hard and error prone beyond simple programs. Apparently I was wrong about
> that, and
I always thought that formal verification (FV) of programs would be too
hard and error prone beyond simple programs. Apparently I was wrong about
that, and one reason is that FV should be applied above the program level -
e.g., to algorithms.
*"TLA+ is a language for modeling software above
