Hacker News: specvsimpl

New comment by specvsimpl in "Do your own writing"

specvsimpl — Tue, 31 Mar 2026 01:54:29 +0000

Maybe they are aware of it?

I talk to other people. They influence me, steer me. I am okay with that.

New comment by specvsimpl in "Do your own writing"

specvsimpl — Tue, 31 Mar 2026 01:44:11 +0000

In a lot of my AI assisted writing, the prompt is an order of magnitude larger than the output.

Prompt: here are 5 websites, 3 articles I wrote, 7 semi-relevant markdown notes, the invitation for the lecture I'm giving, a description of the intended audience, and my personal plan and outline.

Output: draft of a lecture

And then the review, the iteration, feedback loops.

The result is thoroughly a collaboration between me and AI. I am confident that this is getting me past writer blocks, and is helping me build better arcs in my writing and lectures.

The result is also thoroughly what I want to say. If I'm unhappy with parts, then I add more input material, iterate further.

I assure you that I spend hours preparing a 10_min pitch. With AI.

(This comment was produced without AI.)

New comment by specvsimpl in "Further human + AI + proof assistant work on Knuth's "Claude Cycles" problem"

specvsimpl — Sun, 29 Mar 2026 05:03:39 +0000

You are aware of software verification? The AI can prove (mathematically) that its code implements the spec.

New comment by specvsimpl in "Further human + AI + proof assistant work on Knuth's "Claude Cycles" problem"

specvsimpl — Sun, 29 Mar 2026 04:44:38 +0000

I can only say that at family meetings, I hear people talk about contracting with a shop that used to have 4 web designers, but now it's 1 guy, delivering 4x faster than before.

So devs are being replaced.

New comment by specvsimpl in "Leanstral: Open-source agent for trustworthy coding and formal proof engineering"

specvsimpl — Tue, 17 Mar 2026 04:24:18 +0000

Uhm, no? Even with "simple" examples like Dijkstra's shortest path, the spec is easier than the implementation. Maybe not for you, but try it out on an arbitrary 5-yr old. On the extreme end, you have results in maths, like Fermat's Last Theorem. Every teenager can understand the statement (certainly after 10 mins of explanation) but the proof is thousands of pages of super-specialized maths. It is a spectrum. For cryptography, compression, error-correction, databases, etc, the spec is often much simpler than the implementation.