←back to thread

378 points todsacerdoti | 4 comments | | HN request time: 1.202s | source
Show context
mensetmanusman ◴[] No.44984308[source]
Not being a programmer, I have a question.

Can any program be broken down into functions and functions of functions that have inputs and outputs so that they can be verified if they are working?

replies(13): >>44984336 #>>44984354 #>>44984459 #>>44984510 #>>44984549 #>>44984555 #>>44984562 #>>44984865 #>>44984968 #>>44985022 #>>44986774 #>>44988388 #>>45001896 #
cyberpunk ◴[] No.44984336[source]
Pretty much, yes. But what i think you’re talking about (formal verification of code) is a bit of a dark art and barely makes it out of very specialised stuff like warhead guidance computers and maybe some medical stuff etc.
replies(2): >>44984505 #>>44988485 #
timschmidt ◴[] No.44984505[source]
Most people don't bother with formal verification because it costs extra labor and time. LLMs address both. I've been enjoying working with an LLM on Rust projects, especially for writing tests, which aren't the same as formal verification, but it's in the same ballpark.
replies(2): >>44984837 #>>44984891 #
1. cryptonym ◴[] No.44984837[source]
Vibe-coding tests is nowhere near formal verification.
replies(1): >>44998848 #
2. timschmidt ◴[] No.44998848[source]
When typewriters spread in the late 19th century, clerks who used them were sometimes called “mechanical scribblers” or accused of doing “machine work” rather than proper clerical labor.

When adding machines and calculators appeared in offices, detractors claimed they would weaken the mind. In the mid-20th century, some educators derided calculator users as “button pushers” rather than “real mathematicians.”

In the 1980s, early adopters of personal computers and word processors were sometimes called “typists with toys.” Secretaries who mastered word processors were sometimes derided as “not real secretaries” because they lacked shorthand or dictation skills.

Architects and engineers who switched from drafting tables to CAD in the 1970s–80s faced accusations that CAD work was “cookie-cutter” and lacked craftsmanship. Traditional draftsmen argued that “real” design required hand drawing, while CAD users were seen as letting the machine think for them.

Across history, the insults usually follow the same structure:

- Suggesting the new tool makes the work too easy, therefore less valuable.

- Positioning users as “operators” rather than “thinkers.”

- Romanticizing the older skill as more “authentic” or “serious.”

replies(1): >>45024319 #
3. cryptonym ◴[] No.45024319[source]
Few generated unit tests doesn't replace formal verification. That's just not the same thing at all, it's not a matter of manual vs automated calculator.
replies(1): >>45079128 #
4. timschmidt ◴[] No.45079128{3}[source]
> Few generated unit tests doesn't replace formal verification.

That's a claim you're making for the first time, here. Not one I've made. Go ahead and re-read my comments to verify.