This is kind of a tangent, but there are two types of programming that seem like fun little games. On the one hand low-level assembly and on the other hand high-level code that uses logic or type system trickery to prove various correctness or at least some nice properties of the program.
I just hope that someone at some point figures out how to combine these two things, so we can pursue the best possible way of writing a program, and then prove it correct too. This would be a sort-of immortal program that would never need updating. Well, until it becomes obsolete because the world has changed around it.
I am slowly working on a “programmable assembler” for basically this purpose — the hope is to start with making it easier to construct simple binaries while also leaving headroom to build abstractions for proofs as scripts.
Comments
This is kind of a tangent, but there are two types of programming that seem like fun little games. On the one hand low-level assembly and on the other hand high-level code that uses logic or type system trickery to prove various correctness or at least some nice properties of the program.
I just hope that someone at some point figures out how to combine these two things, so we can pursue the best possible way of writing a program, and then prove it correct too. This would be a sort-of immortal program that would never need updating. Well, until it becomes obsolete because the world has changed around it.
I am slowly working on a “programmable assembler” for basically this purpose — the hope is to start with making it easier to construct simple binaries while also leaving headroom to build abstractions for proofs as scripts.