One interesting consequence of the rise of LLMs: there's more demand for tools that handle untrusted input.
Arbitrary HTML+JS can be safely run in a browser. Lean can check an arbitrary proof.
Are there other tools in this family?
miniblog.
Related Posts
1
LLMs have been really helpful for me porting some JS projects to TS.
Since the types are erased and annotations are optional, I can go gradually and safely with more minimal human oversight.
(I'm not sure if it'll significantly help robustness, but it's lovely for navigation.)
32
Show, don't tell: effective advice for writing for both LLMs and people!
2
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.