Would you rather run a formally verified application on top of a conventional kernel/compiler toolchain, or a conventional application on verified kernel/compiler toolchain? Why?
miniblog.
Related Posts
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:
My default assumption is that external libraries are better than what I (or an LLM) would write in a v1.
The extra effort to publish a project generally signifies that the author has spent a good amount of time on the problem. I end up prompting LLMs to prefer external code.
I think you could build an interesting IDE with a tiny embedded LLM in addition to the usual tooling.
Features like 'extract method' would be much nicer if an LLM could provide a name. Choosing a good name is virtually impossible from just a typed AST.
