Follow

if i were a programmer, i would simply predict all the possible states of my program and prevent invalid ones from occurring

@dankwraith I think you're up to something good here

@dankwraith According to the SQLite developers they were paid to do so for a client in the airline industry. Because there's regulation there requiring it.

That regulation though doesn't stop them from implementing terrible ideas.

@alcinnz @dankwraith A programming language required by the aviation industry

@zensaiyuki @dankwraith Oh. I have absolutely no idea.

I just know the example I gave of SQLite is written in C, and is one of the best written codebases I've seen.

@alcinnz @dankwraith sqlite, if it is “correct@, is likely the only correct C program in existence. chances are it’s not 100% correct though, and likely due to certain file systems being incorrect and impossible to work around

@alcinnz @dankwraith in a study that i am struggling to relocate the reference to, some 300 programs were studied and it was found sqlite is the only one that uses the filesystem apis correctly, (correctly not as in math, but as in a way that avoids corruption) and only in one mode.

@wilfredh @alcinnz @dankwraith it’s enough to make me want to use sqlite exclusively instead of the file system unless I absolutely have to use the file system

@zensaiyuki @wilfredh @dankwraith I use SQLite exclusively for my Odysseus web browser, and I'm finding it very expressive.

I hear the hate SQL gets, but (like Haskell) I think that's because that's because they aren't applying it to the right problems.

@alcinnz @dankwraith it’s got a design by contract paradigm. you declare up front what a programming unit it supposed to do, and then it refuses to compile if your actual program doesn’t mathematically resolve against the contract

@zensaiyuki @dankwraith Oh! One of my university lecturers is writing a language at least somewhat like that: Whiley.

It would be a useful tool to have in our toolbox!

@alcinnz @dankwraith ADA was once a legal requirement for all progtams in the aviation industry because in principle, all programs written in it are “correct”
(or they don’t compile)
i don’t know the details but i suspect the definition of “correct” here wasn’t 100% satisfactory

@alcinnz @dankwraith in a way, Ada is a direct answer to the first toot in the thread: let the computer evaluate all possible states of the program from a soec, and then slap your wrist with a ruler at a steadypace until you get it right

@zensaiyuki @alcinnz @dankwraith The details are that ADA is just a Pascal-like with a great type system and module system for the time. There is no theorem prover or anything fancy like that in there.

@dankwraith lol no joke as a kid i thought that to make a video game programmers created every possible image that could be shown on screen

@dankwraith
It genuinely made me smile, the same kind of smiling when thinking about a pure and wonderful utopy were no harm is made to anything and everything is nice.

And then there are things like C++, lurking in a corner, waiting for the best moment to trap you with an undefined behaviour due to some implicit conversion between obscure xlrgvalue magic...

@dankwraith One day, a guy in the customer support department asked me why I don't do exactly that. Indeed, why don't I?

@dankwraith if i were a programmer with a sensible trade union i would simply import and configure the appropriate state machine which union engineers have subjected to a rigorous audit and which the union trained me to use

@dankwraith This is legit what good programmers are supposed to do. I do it all the time as I write code. Sadly, poor documentation in libraries can limit how far you can go with this though. This is why I try to go as far as I can with glibc and if I ever write code, I document it to death.

@dankwraith Generally that's what I do.

Normally I don't encounter crashes on deployed code.

@dankwraith make's u wonder,,, why the pointty headid nerd's never DO that!!!! proggraming, its a SCAM

@dankwraith We do!

0
1
Broken

The problem is Broken is always a valid state.

Sign in to participate in the conversation
monads.online

monads.online is one server in the network