Yoichi Hirai
@pirapira.bsky.social
interested in computation and logic.
I was comparing formal verification frameworks for arithmetic circuits: blog.zksecurity.xyz/posts/formal...
Comparison of formal verification frameworks for arithmetic circuits
A hands-on comparison of formal verification frameworks for arithmetic circuits, evaluating those in the ACL2 Book (r1cs, PFCS), acl2-jolt, Garden (Rocq), zk-lean, sp1-lean, and Clean. Each framework ...
blog.zksecurity.xyz
November 23, 2025 at 9:02 PM
I was comparing formal verification frameworks for arithmetic circuits: blog.zksecurity.xyz/posts/formal...
Math is the archetype reasonable system. People are gathering statements = specifications: mathstodon.xyz/@tao/1145865...
May 29, 2025 at 4:48 PM
Math is the archetype reasonable system. People are gathering statements = specifications: mathstodon.xyz/@tao/1145865...
My reasonable engineering manifesto is still changing. github.com/pirapira/rea...
GitHub - pirapira/reasonable-manifesto: Reasonable Engineering Manifest
Reasonable Engineering Manifest. Contribute to pirapira/reasonable-manifesto development by creating an account on GitHub.
github.com
May 12, 2025 at 10:59 AM
My reasonable engineering manifesto is still changing. github.com/pirapira/rea...
sounds like it's getting there.
Once getting QED is automated, the bottleneck is me wanting statements to be proven. I will want statements proven about things with short specifications: the reasonable systems.
I'm making up a technical term called reasonable systems. A reasonable system can be reasoned about with theorem provers, SMT solvers, model checkers or such. The behavior of a reasonable system can be described with a relatively small amount of logical formulas.
May 1, 2025 at 9:31 PM
sounds like it's getting there.
My reasonable engineering manifesto is getting in shape. I'll edit it a bit more. github.com/pirapira/rea...
GitHub - pirapira/reasonable-manifesto: Reasonable Engineering Manifest
Reasonable Engineering Manifest. Contribute to pirapira/reasonable-manifesto development by creating an account on GitHub.
github.com
April 12, 2025 at 11:11 PM
My reasonable engineering manifesto is getting in shape. I'll edit it a bit more. github.com/pirapira/rea...
I started writing reasonable manifesto for systems that can be reasoned about github.com/pirapira/rea...
GitHub - pirapira/reasonable-manifesto: Reasonable Manifest
Reasonable Manifest. Contribute to pirapira/reasonable-manifesto development by creating an account on GitHub.
github.com
April 12, 2025 at 10:54 AM
I started writing reasonable manifesto for systems that can be reasoned about github.com/pirapira/rea...
Once getting QED is automated, the bottleneck is me wanting statements to be proven. I will want statements proven about things with short specifications: the reasonable systems.
I'm making up a technical term called reasonable systems. A reasonable system can be reasoned about with theorem provers, SMT solvers, model checkers or such. The behavior of a reasonable system can be described with a relatively small amount of logical formulas.
January 12, 2025 at 11:45 PM
Once getting QED is automated, the bottleneck is me wanting statements to be proven. I will want statements proven about things with short specifications: the reasonable systems.
I ignored navigation apps and found a nice ride.
October 15, 2023 at 7:42 PM
I ignored navigation apps and found a nice ride.
Reposted by Yoichi Hirai
If something is described as avocado green, how are you supposed to know if that means outside or inside?
August 22, 2023 at 4:43 PM
If something is described as avocado green, how are you supposed to know if that means outside or inside?
Reposted by Yoichi Hirai
You can get bedsheets made with RFC printed on it
July 22, 2023 at 12:14 AM
You can get bedsheets made with RFC printed on it
「朝のドラめもん」くらい安定した質のものを毎日書いて何十年にもわたって公表するのは、よいなと思う。公表の媒体も、テキストだけのHTMLを自分のWebサーバに置くだけで、長期的に維持するのに向いていてよいなと思う。
July 22, 2023 at 9:43 AM
「朝のドラめもん」くらい安定した質のものを毎日書いて何十年にもわたって公表するのは、よいなと思う。公表の媒体も、テキストだけのHTMLを自分のWebサーバに置くだけで、長期的に維持するのに向いていてよいなと思う。
I'm making up a technical term called reasonable systems. A reasonable system can be reasoned about with theorem provers, SMT solvers, model checkers or such. The behavior of a reasonable system can be described with a relatively small amount of logical formulas.
July 16, 2023 at 8:41 PM
I'm making up a technical term called reasonable systems. A reasonable system can be reasoned about with theorem provers, SMT solvers, model checkers or such. The behavior of a reasonable system can be described with a relatively small amount of logical formulas.
Ein Tipp gegen die Hitze: Nutze den südlichen Gehweg. Dieser liegt öfter im Schatten.
July 16, 2023 at 8:34 PM
Ein Tipp gegen die Hitze: Nutze den südlichen Gehweg. Dieser liegt öfter im Schatten.