News for hackers. Stuff that matters.

A comment on Lean proved this program correct; then I found a bug. Parent comment

Re:Lean proved this program correct; then I found a bug by gopiandcode on Monday April 13, 2026 @10:36PM (#47760599)
you can still verify arbitrarily long running programs - there are instances of such software, such as sel4 (https://sel4.systems/) and certikos (https://flint.cs.yale.edu/certikos/), you simply model them as finite programs that run on an infinite stream of events.
[ Parent | on HN ]
Re:Lean proved this program correct; then I found a bug by DonaldPShimoda on Tuesday April 14, 2026 @12:18PM (#47767621)
> finite programs that run on an infinite stream of events

This requires coinduction, right? (That's my understanding of the formal representation of infinite streams.) If so, that does limit your options, since most of the proof assistants don't handle coinductive data, as I understand it.

[ Parent | on HN ]