Margaret Hamilton and her team took Apollo 11 to the moon using assembly language. I like to think about that when people say that it's impossible to write a correct program in assembly or C.
Preparing for incoming Opinions. :)
@alva also, her child did quality assurance!
@malte I didn't know that :D
@alva she encouraged her child to play with the software to find errors in boundary checks etc, which the child of course did!
when hamilton went to her managers to approve a fix, they told her that none of the astronauts would ever make such [ableist/patronizing adjective] data entry mistakes... do i have to spell out the rest of the story? 😏😒😏😒🤓
@malte Manual fuzzing
@alva you can write a correct program in assembly
but not in C
@hirojin So if I write a program in C that results in the exact same code as the assembly version, it is somehow less correct?
but good luck trying!
(hello world doesn't count)
@hirojin I think I would trust a formally verified C program over a Rust one verified by "it compiled." :)
I listened to an interview of a guy who works on formal verification software for C, which is itself written in C++. They asked him if they had ever turned their software on itself. Oh, no, we couldn't possibly do formal verification of C++ - the language is just too complex.
Felt ironic to me.
@alva that feels like a weird dichotomy: why couldn't the rust program also be formally verified?
i understand that much of propaganda out there is just rewrite it in Rust, and it'll be perfect
but if we look at the general communities, there's very little awareness of how unreliable one's knowledge is as to what a program turn into, once it passes thru the compiler
at least the rust compiler is direct and honest about this, instead of trying to aid you in your delusions
@hirojin I guess it could (or could it? I don't know the state of Rust as it pertains to verification) but like you said, I never see Rust people talking about anything that could offer more assurance. Anything below Rust is too little, and anything above it is too much, it seems. Being a responsible programmer who writes correct programs means exactly "it passed rustc," is the impression I get a lot of the time.
and then there's people trying to make it so that rustc can prove… something about unsafe within Rust's type system
but, yeah, that still leaves us with LLVM…
LLVM needs to be formally verified.
not just for Rust's sake, but for the sake of all languages that build on top of it.
@hirojin Also, C programmers who are the least bit concerned about the correctness of their program, don't just send it through GCC/Clang and call it a day. At least not in my experience.
@alva most C programmers i had the joy talking to don't (just) trust the compiler, they trust themselves even more to know what the result of their program will be — without even using any of those compiler flags (that might prove them wrong, with those annoying warnings)
so perhaps we have had bei different experience with programmers, which makes sense, since i've mostly worked in ops
@hirojin Well, that doesn't sound good. Maybe I've been really lucky then. My coworkers (and I) have used various tools and techniques at our disposal, that give fairly high return on investment. Some of them go beyond what rustc offers, for some specific issues (like alignment.) I'm not saying that Rust isn't a safer default; I just don't believe that a language alone will save us, and if someone puts the responsibility of correctness entirely on rustc, I can't trust them.
@alva there's still semantic / logical correctness
some of that can be caught with stuff like: https://www.viva64.com/en/pvs-studio/
look, working in ops, you usually only get to work with the worst programmers
cuz the best programmers' programs don't wake you up
which makes you think only bad programmers exist
@alva @hirojin dunno if you already saw things like https://people.mpi-sws.org/~dreyer/papers/rustbelt/paper.pdf and https://internals.rust-lang.org/t/announcing-the-formal-verification-working-group/7240
They are doing awesome work.
@alva @hirojin I don't think it's fair to say Rust devs rely on the compiler alone. At minimum most projects have unit tests because Rust makes that super convenient. Its property and fuzz testing tools are great and widely used as well, and those techniques find a lot of the bugs formal verification would at less cost. I have more nuanced things to say about that but I already said them in this talk: https://www.youtube.com/watch?v=zhhtQ_-t1pw
Also the https://github.com/tokio-rs/loom concurrent model checker is being used for things a lot of people rely on, which I haven't seen happen in any other language.
I'd certainly like to see more tools for building trustworthy software. I had a team of students build https://github.com/Rust-Proof/rustproof a few years ago to add one kind of formal verification to Rust. That prototype relied on compiler internals, but at this point Rust's support for procedural macros might let this be done on stable Rust. Hmm, I should look into that.
I do have a lot of sympathy for the view that it's impossible to write correct code in C—even though "impossible" is clearly an exaggeration—given the sorts of issues folks like John Regehr study, such as https://blog.regehr.org/archives/1520 or https://blog.regehr.org/archives/1466
Of course, this was done as a research project to demonstrate that formally-proven code could be an order-of-magnitude cheaper than the state of the art.
And it succeeded! It only cost $1,000 per line of code, instead of $10,000!
It's not impossible to write a non-trivial program correctly in C. It's just impractically expensive.
@alva I think everyone should play TIS-100 at least once.
@alva Margaret Hamilton was awesome.
That's it, that's my Opinion.
@alva argh, i got an anxiety spike on your behalf when you posted that
@kiilas I closed the Mastodon tab for the night, and when I came back today there were some replies, but mostly sensible ones. Surprising!
@alva It's certainly possible to write a correct program like that, but the compiler absolutely won't help you with it
@LunaDragofelis Yeah. It's just that some people say it's literally impossible. Not hard, not you need to employ formal verification methods, just impossible.
Do you think I'm as mentally capable, and rigorous with my code, as Hamilton?
That said, as long as security's not a concern I probably could write a correct program in C.
@alva the original roller-coaster tycoon was written in 99% assembly and 1% c, which is a pretty good fuck you to people who think real things can't be written in it
That doesn't mean that assembler is a great choice for sensitive applications. If anyone ways it's impossible to write correct code in assembler or C, they are indeed idiots. But that doesn't mean there are better choices if the goal is to minimise critical errors.
I'd also like yo point out that certain people (especially Rust fans) tend to believe that the only type of errors that can cause critical failures is memory overruns. Memory errors doesn't happen in any major programming language (except for C and C++) so it's really not an interesting problem to solve.
Formal verification is interesting, and can help, but writing formally verified code is very expensive so it's reversed for the critical code. Also, formal verification only verifies that the program behaves according to the specification. It does not ensure that the specification correctly described the requirements.
> Memory errors doesn't happen in any major programming language [..] so it's really not an interesting problem to solve
What makes #rust's approach interesting is that it doesn't require a VM, and an associated performance hit.
first of all, programs (or languages, or frameworks, or servers) written in garbage collected languages can leak memory — and how!
secondly, well written java programs can run faster than their C equivalent, unless you compile to the native CPU, AND profile it, which is what JIT compiler does
@isagalaev @Eden @alva I don't disagree that the Rust approach is interesting. I do find it interesting from a mostly academic standpoint, because in practice there are actually very few real problems that Rust is the ideal solution for.
I also need to point out that the suggestion you made that garbage collection requires a VM is not correct. I do a lot of development in Common Lisp using SBCL which is a dynamic language that compiles directly to native machine code but is garbage collected.
There are other examples which are statically compiled and also garbage collected, for example Go or D.
@alva Aye, not impossible, just hard.
Further, I think I'd argue that it's impossible to write *any* correct [nontrivial] program, in anything.
At some point, a [organic] brain has to specify the problem to solve, in some language such that the problem can be given to a computer.
The brain can and will make a bunch of mistakes as it does this.
A formal proof still needs to include a problem specification, so it will include errors.
If I write a C program with a formal proof, there are likely to be a few errors in common between the C and the formal proof, so that my program is *still* wrong!
Maybe I've just misunderstood how formal proof works :3
One interesting aspect is that a lot of the code wasn't written in native assembly for the AGC. Instead they implemented a virtual machine whose language washed still very much like assembler, but was not much more easy to use than the native code. For example, the virtual machine implemented support for double precision values and vector maths.
It also gave me you things like pointer indexing which the native code of the AGC didn't have (it had a weird INDEX instruction which allowed you to achieve this, but it was very hard to use).
I was reading the flight journal of Apollo 13, it's really engrossing. And I like how they refer to the code in terms of Verbs and Nouns.
"057:21:54 Lousma: 13, Houston. We're ready with a Verb 74 now, please. [Pause.]
057:22:05 Swigert: Coming down at you.
[Verb 74 begins the dump of the computer's erasable 2K word memory to Earth.]"
Beach City is our private beach-side sanctuary for close friends and awesome folks. We are various flavors of trans, queer, non-binary, polyamorous, disabled, furry, etc.