←back to thread

What is going on right now?

(catskull.net)
378 points todsacerdoti | 2 comments | 22 Aug 25 07:08 UTC | HN request time: 0.482s | source
Show context
mensetmanusman ◴[22 Aug 25 13:18 UTC] 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 ◴[22 Aug 25 13:20 UTC] 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 #
1. chasd00 ◴[22 Aug 25 19:03 UTC] No.44988485[source]▶
Also, if you're going to formally verify your code then the compiler better have been formally verified. If the compiler has been verified then the ASM better be formally verified and so on all the way down to the actual circuit and clock.

...then a bit flips because of a stray high energy particle or someone trips over the metaphorical power cord and it all crashes anyway.

replies(1): >>45010568 #
2. cyberpunk ◴[25 Aug 25 05:37 UTC] No.45010568[source]▶
Actually I knew someone who worked on special compilers for embedded stuff for the military which would only emit code which uses specific asm operations which had been verified on specific cpus.

So it’s really not that far fetched.