miniblog.

← Back to all posts
Dec 25, 2017 at 00:12
Formal Verification: The Gap Between Perfect Code and Reality https://raywang.tech/2017/12/20/Formal-Verification:-The-Gap-between-Perfect-Code-and-Reality/ Good critique of how formal verification techniques can be extremely heavyweight. Also discusses (rather pessimistically) how it's important to know which parts are not verified
Formal Verification: The Gap Between Perfect Code and Reality
Formal Verification: The Gap Between Perfect Code and Reality
Thanks to Vlad Brown and Drawings Team for Russian and Uzbek translations. In Fall 2017, I took MIT’s 6.826, Principles of Computer Systems, taught by Turing Award-winner Butler Lampson, Nickolai Z

Related Posts

Feb 7, 2026 at 20:55
1
Today I learnt about "bypass charging", a phone feature where it can run directly off the mains without using the battery at all. No battery charging, less heat, less battery wear. Nifty.
Here are all the phones that support bypass charging, and why you should use it
Here are all the phones that support bypass charging, and why you should use it
Few phones on the market can draw power directly from the wall, bypassing the battery while charging. But are the benefits tangible enough?
Feb 5, 2026 at 23:09
1
I'm considering using WebP more: for example, my websites would load faster and browsers have supported it since 2020: https://caniuse.com/webp That said, GitHub just added support in August 2025, so I suspect I'd still find use cases that don't work yet:
WebP image format | Can I use... Support tables for HTML5, CSS3, etc
"Can I use" provides up-to-date browser support tables for support of front-end web technologies on desktop and mobile web browsers.
Added support for WebP images - GitHub Changelog
Added support for WebP images - GitHub Changelog
WebP image support is now available across github.com and GitHub Enterprise Cloud with data residency. Previously, uploading WebP images resulted in broken previews or forced users to download files to…
Feb 5, 2026 at 09:59
3
Test code is total: we require it to always terminate or it's a failure! It also typically has 100% line and branch coverage. I feel way less nervous about refactoring tests, you can always just run them.