Path: csiph.com!eternal-september.org!feeder.eternal-september.org!nntp.eternal-september.org!.POSTED!not-for-mail
From: Paul Rubin <no.email@nospam.invalid>
Newsgroups: comp.lang.forth
Subject: Re: First result in riscv optimiser
Date: Fri, 11 Sep 2026 17:09:19 -0700
Organization: A noiseless patient Spider
Lines: 9
Message-ID: <87cxujjpow.fsf@nightsong.com>
References: <nnd$172defd2$1b2df6f6@e430673098f06a19> <87ecf96ljg.fsf@debian> <nnd$23c5006f$6f768ed1@9c6c99f017e8c6d5> <87y0dcgvxf.fsf@debian> <nnd$2a0f5231$3093e519@df6cdc0aa2637ff7> <877bksdpui.fsf@debian>
MIME-Version: 1.0
Content-Type: text/plain
Injection-Date: Sat, 12 Sep 2026 00:09:20 +0000 (UTC)
Injection-Info: dont-email.me; logging-data="3510250"; mail-complaints-to="abuse@eternal-september.org";	posting-account="U2FsdGVkX197LukzWXpoMGqdIlmbatOn"; posting-host="605061d606f2312cb00f7b420c549432"
User-Agent: Gnus/5.13 (Gnus v5.13) Emacs/27.1 (gnu/linux)
Cancel-Lock: sha1:QR12rjZdh3a2KcEy3v6lpVi+qwc= sha1:5694gKafkoW+5ynLfOc02Orxom0= sha256:lpKhHDIzHTDWCsY51ct7f7WWz83zQySCC3M88qTbGOA= sha1:1Vj7KeSKSBEePvEpIV4MmBcFh/c= sha256:C35jPOIsDNnIIK72rqzQhPtsVKAMOnpxbxA9ocqe/IA=
Xref: csiph.com comp.lang.forth:135677

Kragen Javier Sitaker <kragen@canonical.org> writes:
>> I have 106 peephole patterns, some quite complicated.
> How confident are you that all 106 are correct?

It's sometimes possible to use SAT solvers to prove that two code
sequences are equivalent, without much human input.  There are also
formal models of RISC-V that you can put into a proof assistant.  Or
these days maybe you can throw the whole set into an LLM and ask for
formal proofs.