formats over apps

i also explicitly instruct llm to try to maintain the mapping so the code reads 1:1. and finally i specifically tell LLM to isolate all "runnable" code in separate files from proofs, with file names 1:1 matching original JS names. so when it discovers code it kind of "notices" these are all mapped

yes but if you write "mutable" code in Lean, it unrolls to State monad anyway, and Lean can prove things about that easily, like pre/post-conditions etc. the much more difficult challenge is how to model and prove higher level behaviors of entire program.

i vibed a test suite runner that let me annotate Lean functions with a declarative attribute that specifies which JS function it corresponds to, and which Lean state and JS state to capture as we enter/leave. then it runs many scenarios against Lean and JS and verifies traces match

there’s a lot of things in the middle that i should write about when/if i get it working to the extent i want. i’ve gotten good partial results but not sufficient to claim victory.

it depends (tm) you need a sufficient mathematical (Lean) model of the “things” you want to state “facts” about. you’d define them with inductive types, Props, structures — same as usual in Lean then you define a Lean version of your code. and try to prove that it instantiates those laws

i’ve been doing some research on using Lean with AI to prove software properties (in my case, pieces of React). i’ll try to share lessons if it gets to a useful state. the main thing i’m learning is that, with this setup, proofs are *grown*. you can’t “just build them”

my impression is that the author doesn’t mean it in the sense “these two things are super similar!” but more like “here’s a crude speculative reframing that forces you to abandon similarly crude-but-enshrined intuitions that are prevalent today“

oh yeah i agree tables are cringe (i skipped them). i mostly liked the rest though

can you give an example of where it feels painful?

this too

fun read

i think today frontier level models will be available as open weights in a few years, and then it's going to be wild west?

been unironically upping my p doom over the last few months

in my experience, AI is excelling at most technical work except for ”what is the right next problem to work on”. for now, humans still have a noticeable advantage there

hey this album slaps