News for hackers. Stuff that matters.

A comment on Debugging in the Multiverse. Parent comment

Re:Debugging in the Multiverse by formalspec on Wednesday September 11, 2024 @12:22AM (#41507996)
> No language will prevent you from misimplementing the specs

If the spec is written in the language itself, then some languages certainly will.

See Lean, Rocq, Isabelle, etc

[ Parent | on HN ]
Re:Debugging in the Multiverse by svieira on Wednesday September 11, 2024 @12:17PM (#41512796)
Unfortunately we do not yet have a way to write reality in any of these languages, so there is always at-least-one-level of translation where errors in representation may creep in.
[ Parent | on HN ]