A remarkable post introducing a GHC plugin that proves your programs obey laws: https://www.joachim-breitner.de/blog/717-Why_prove_programs_equivalent_when_your_compiler_can_do_that_for_you_
Related Posts
Claude asked me a question today: was I looking for an Emacs plugin (because I was talking about elisp) or a Rust program (because I have configured Rust preferences)?
I'm really impressed, it's rare to see LLMs ask follow-up questions.
(I wanted Emacs in this case.)
I would have thought that invoking a C compiler would be a solved problem. Looking at Rust's cc crate there's a remarkable long tail of corner cases to fix.
Exotic CPUs, microarchitectures, compiler differences, operating system differences, etc.
https://github.com/rust-lang/cc-rs/blob/main/CHANGELOG.md
I'm implementing an interpreter, and wondering how often I should check for interruptions (e.g. Ctrl-C).
I don't want to spend too much CPU time checking whether I've been interrupted, but I also want slow programs to stop promptly. It's tricky.