I don’t know about making god software, but human software is a lot of trial and error. I have been writing code for close to 40 years. The best I can do is write automated tests to anticipate the kinds of errors I might get. My imagination just isn’t as strong as reality.
I think it is incorrect to say that testing things fully formally is the only alternative to whatever the heck we are currently doing. I mean there is property-based testing as a first step (which maybe you also refer to with automated tests but I would guess you are probably mainly talking about unit tests).
Maybe try Haskell or even better Idris? The Haskell compiler is very annoying until you realize that it loves you. Each time it annoys you with compile errors it actually says “Look I found this error here that I am very very sure you’d agree is an error, so let me not produce this machine code that would do things you don’t want it to do”.
It’s very bad at communicating this though, so it’s words of love usually are blurted out like this:
Don’t bother understanding the details, they are not important.
So maybe Haskell’s greatest strength, being a very “noisy” compiler, is also its downfall. Nobody likes being told that they are wrong, well at least not until you understand that your goals and the compiler’s goals are actually aligned. And the compiler is just better at thinking about certain kinds of things that are harder for you to think about.
In Haskell, you don’t really ever try to prove anything about your program in your program. All of this you get by just using the language normally. You can then go one step further with Agda, Idris2, or Lean, and start to prove things about your programs, which easily can get tedious.
But even then when you have dependent types you can just add a lot more information to your types, which makes the compiler able to help you better. Really we could see it as an improvement to how you can tell the compiler what you want.
But again, you what you can do in dependent type theory? NOT use dependent type theory! You can use Haskell-style code in Idris whenever that is more convenient.
And by the way, I totally agree that all of these languages I named are probably only ghostly images of what they could truly be. But I guess humanity cares more about making javascript run REALLY REALLY FAST.
And I got to be careful not to go there.
I feel you on being distracted by software bugs. I’m one of those guys that reports them, or even code change suggestions (GitHub Pull Requests).
Yeah, I also do this. My experience so far generally has been very positive. It’s really cool when I make an issue with “I would think it would be nice if this program does X”, and then have it do x in 1 or 2 weeks.
I don’t know where to open an issue though about that I think it would be better to not build a god we don’t comprehend. Maybe I haven’t looked hard enough.
Haskell is a beautiful language, but in my admittedly limited experience it’s been quite hard to reason about memory usage in deployed software (which is important because programs run on physical hardware. No matter how beautiful your abstract machine, you will run into issues where the assumptions that abstraction makes don’t match reality).
That’s not to say more robust programming languages aren’t possible. IMO rust is quite nice, and easily interoperable with a lot of existing code, which is probably a major factor in why it’s seeing much higher adoption.
But to echo and build off what @ustice said earlier:
The hard part of programming isn’t writing a program that transforms simple inputs with fully known properties into simple outputs that are meet some known requirement. The hard parts are finding or creating a mostly-non-leaky abstraction that maps well onto your inputs, and determining what precise machine-interpretable rules produce outputs that look like the ones you want.
Most bugs I’ve seen come at the boundaries of the system, where it turns out that one of your assumptions about your inputs was wrong, or that one of your assumptions about how your outputs will be used was wrong.
I almost never see bugs like this
My sort(list, comparison_fn) function fails to correctly sort the list”
My graph traversal algorithm skips nodes it should have hit
My pick_winning_poker_hand() function doesn’t always recognize straights
Instead, I usually see stuff like
My program assumes that when the server receives an order_received webhook, and then hits the server to fetch the order details from the vendor’s API for the order identified in the webhook payload, the vendor’s API will return the order details and not a 404 not found”
My server returns nothing at all when fetching the user’s bill for this month, because while the logic is correct (determine the amount due for each order and sum), this particular user had 350,000 individual orders this month so the endpoint takes >30 seconds, times out, and returns nothing.
The program takes satellite images along with Metadata that includes the exact timesamp, which satellite took the picture, and how the satellite was angles. It identifies locations which match a specific feature, and spits out a latitude, longitude, label, and confidence score. However, when viewing the locations on a map, they appear to be 100-700 meters off, but only for points within the borders of China (because the programmer didn’t know about GCJ-02)
Programming languages that help you write code that is “correct” mostly help prevent the first type of bug, not the second.
Another thing that Haskell would not help you at all with is making your application good. Haskell would not force obsidian to have unbreakable references.
I think it is incorrect to say that testing things fully formally is the only alternative to whatever the heck we are currently doing. I mean there is property-based testing as a first step (which maybe you also refer to with automated tests but I would guess you are probably mainly talking about unit tests).
Maybe try Haskell or even better Idris? The Haskell compiler is very annoying until you realize that it loves you. Each time it annoys you with compile errors it actually says “Look I found this error here that I am very very sure you’d agree is an error, so let me not produce this machine code that would do things you don’t want it to do”.
It’s very bad at communicating this though, so it’s words of love usually are blurted out like this:
Don’t bother understanding the details, they are not important.
So maybe Haskell’s greatest strength, being a very “noisy” compiler, is also its downfall. Nobody likes being told that they are wrong, well at least not until you understand that your goals and the compiler’s goals are actually aligned. And the compiler is just better at thinking about certain kinds of things that are harder for you to think about.
In Haskell, you don’t really ever try to prove anything about your program in your program. All of this you get by just using the language normally. You can then go one step further with Agda, Idris2, or Lean, and start to prove things about your programs, which easily can get tedious.
But even then when you have dependent types you can just add a lot more information to your types, which makes the compiler able to help you better. Really we could see it as an improvement to how you can tell the compiler what you want.
But again, you what you can do in dependent type theory? NOT use dependent type theory! You can use Haskell-style code in Idris whenever that is more convenient.
And by the way, I totally agree that all of these languages I named are probably only ghostly images of what they could truly be. But I guess humanity cares more about making javascript run REALLY REALLY FAST.
And I got to be careful not to go there.
Yeah, I also do this. My experience so far generally has been very positive. It’s really cool when I make an issue with “I would think it would be nice if this program does X”, and then have it do x in 1 or 2 weeks.
I don’t know where to open an issue though about that I think it would be better to not build a god we don’t comprehend. Maybe I haven’t looked hard enough.
Haskell is a beautiful language, but in my admittedly limited experience it’s been quite hard to reason about memory usage in deployed software (which is important because programs run on physical hardware. No matter how beautiful your abstract machine, you will run into issues where the assumptions that abstraction makes don’t match reality).
That’s not to say more robust programming languages aren’t possible. IMO rust is quite nice, and easily interoperable with a lot of existing code, which is probably a major factor in why it’s seeing much higher adoption.
But to echo and build off what @ustice said earlier:
The hard part of programming isn’t writing a program that transforms simple inputs with fully known properties into simple outputs that are meet some known requirement. The hard parts are finding or creating a mostly-non-leaky abstraction that maps well onto your inputs, and determining what precise machine-interpretable rules produce outputs that look like the ones you want.
Most bugs I’ve seen come at the boundaries of the system, where it turns out that one of your assumptions about your inputs was wrong, or that one of your assumptions about how your outputs will be used was wrong.
I almost never see bugs like this
My
sort(list, comparison_fn)function fails to correctly sort the list”My graph traversal algorithm skips nodes it should have hit
My
pick_winning_poker_hand()function doesn’t always recognize straightsInstead, I usually see stuff like
My program assumes that when the server receives an
order_receivedwebhook, and then hits the server to fetch the order details from the vendor’s API for the order identified in the webhook payload, the vendor’s API will return the order details and not a 404 not found”My server returns nothing at all when fetching the user’s bill for this month, because while the logic is correct (determine the amount due for each order and sum), this particular user had 350,000 individual orders this month so the endpoint takes >30 seconds, times out, and returns nothing.
The program takes satellite images along with Metadata that includes the exact timesamp, which satellite took the picture, and how the satellite was angles. It identifies locations which match a specific feature, and spits out a latitude, longitude, label, and confidence score. However, when viewing the locations on a map, they appear to be 100-700 meters off, but only for points within the borders of China (because the programmer didn’t know about GCJ-02)
Programming languages that help you write code that is “correct” mostly help prevent the first type of bug, not the second.
Another thing that Haskell would not help you at all with is making your application good. Haskell would not force obsidian to have unbreakable references.