miniblog.

← Back to all posts
Jul 11, 2016 at 18:29
A remarkable paper just uploaded to arXiv: *proving* that refactoring tools don't break C code!
Renaming Global Variables in C Mechanically Proved Correct
Renaming Global Variables in C Mechanically Proved Correct
Most integrated development environments are shipped with refactoring tools. However, their refactoring operations are often known to be unreliable. As a consequence, developers have to test their code after applying an automatic refactoring. In this article, we consider a refactoring operation (renaming of global variables in C), and we prove that its core implementation preserves the set of possible behaviors of transformed programs. That proof of correctness relies on the operational semantics of C provided by CompCert C in Coq.

Related Posts

Oct 5, 2025 at 20:23
2
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.
cc-rs/CHANGELOG.md at main · rust-lang/cc-rs
cc-rs/CHANGELOG.md at main · rust-lang/cc-rs
Rust library for build scripts to compile C/C++ code into a Rust library - rust-lang/cc-rs
Dec 10, 2022 at 20:31
One remarkable aspect of the JS packaging ecosystem is that people package individual functions. For example, lodash.sortby: https://www.npmjs.com/package/lodash.sortby It shows how lightweight the packaging process is. I've not seen this happen in other ecosystems.
Just a moment...
Nov 23, 2022 at 07:37
Smalltalk has a remarkable method named #become: that allows you to modify all pointers to a given object to point to a different object! https://gbracha.blogspot.com/2009/07/miracle-of-become.html This goes even further than updating instances when a class changes, it's changing instance references.
Room 101: The Miracle of become: