Another thing you're not addressing here is basically Type checking solves none of the problems you describe. You claim it's extraordinarily hard to write tests for UI and for memory corruption. And that's your argument for type checkers? It's next to impossible to type check UI and memory corruption. So your argument has no point here.
SQlite is written in C. It has type checking. Yet people still write unit tests for it. Why? Because type checking is mostly practically inconsequential. All your points don't prove anything. It proves my point.
All the problems you talk about can be solved with more advanced proof based checkers. These systems can literally proof check your entire program to be fully in spec precompile time. It goes far beyond just types. Agda, Idris, Coq, and Microsofts lean have facilities to prove your programs to be fully correct 100% of the time. They exist. But they're not popular. And there's a reason for that.
You say it's paramount to move error detection to compile time. I say, this problem is ALREADY solved, but remains unused because these methods aren't PRACTICAL.
Incorrect. Have a look at the Swift OpenCombine library. Multiple Publishers of a particular type that emits a single boolean value (e.g., an "Agree to Terms" UI checkmark and an "Agree to Privacy Policy" UI checkmark) are combined at compile-time to be transformed into a single Publisher of a type that emits only a single boolean value (e.g., the enabled/disabled state of a "Submit" button). Effectively, it is not possible to even compile an app that incorrectly ignores one of the "Agree" checkmarks before enabling/disabling the "Submit" button.
> It's next to impossible to type check (...) memory corruption
Incorrect. Have a look at the Rust standard library. Sharing data across multiple treads requires passing a multi-threaded Mutex type; attempting to share data through a single-threaded Rc (reference-counted) type will not compile. Once the Mutex type is passed, each thread can only access the memory the Mutex type represents by acquiring another type, a MutexGuard, through locking. Effectively, it is not possible to even compile a program that incorrectly ignores multi-threading or incorrectly accesses memory in a race condition with other threads thus possibly corrupting that memory. Moreover, it is also not possible for a thread not to properly release a lock once the MutexGuard type goes out of scope.
> All the problems you talk about can be solved with more advanced proof based checkers.
Unlikely. Without feeding strong type information that describes your problem domain into a checker, the checker cannot reason about your code and figure out possible errors. A strong type system is a "language" for a programmer to communicate with his or her checker.
> You say it's paramount to move error detection to compile time. I say, this problem is ALREADY solved, but remains unused because these methods aren't PRACTICAL.
> [the C language] has type checking. Yet people still write unit tests for it. Why? Because type checking is mostly practically inconsequential.
Please do not hold it against me if I do not continue commenting here - you must be from a different, parallel Universe. (How is Elvis doin' on your end? ;) J/K)
>Incorrect. Have a look at the Swift OpenCombine library. Multiple Publishers of a particular type that emits a single boolean value
First off types can't emmit values. Types don't exist at run time. They're simply meta info for the compiler to run checks. Thus they can't emmit anything. Second if you're talking about something that emmits a value then it involves logic that doesn't have to do with UI. A UI is not about logic, it is simply a presentation given to the user, all logic is handled by things that AREN'T UI based.
UI would be like html and css. Can you type check html and css make sure the hackernews UI is correct? There is no definition of correctness in UI thus it can't be type checked. The example you're talking about is actually type checking the logic UNDERNEATH the UI.
>Effectively, it is not possible to even compile a program that incorrectly ignores multi-threading or incorrectly accesses memory in a race condition with other threads thus possibly corrupting that memory. Moreover, it is also not possible for a thread not to properly release a lock once the MutexGuard type goes out of scope.
This is different. It's not type checking memory corruption. It's preventing certain race conditions by restricting your code such that you can't create a race condition. There's a subtle difference here. You can violate Rusts constraints in C++ yet still have correct code. Type checking memory corruption would involve code that actually HAS a memory corruption, and some checker proving it has a memory violation. My statement still stands Memory corruption cannot be type checked.
Think about it. A memory corruption is an error because we interpret to be an error. Logically it's not an error. The code is doing what you told it to do. You can't check for an error that's interpreted.
At best you can only restrict your code such that ownership lives in a single thread and a single function which prevents certain race conditions. which is what rust does. This has a cost such that implementing doubly linked lists are a hugely over complicated in rust: https://news.ycombinator.com/item?id=16442743. Safety at the cost of highly restricting the expressiveness of the language is very different from type checking. Type checking literally finds type errors in your code, borrow checking does NOT find memory corruption... it prevents certain corruption from happening that's about it.
>Unlikely. Without feeding strong type information that describes your problem domain into a checker, the checker cannot reason about your code and figure out possible errors. A strong type system is a "language" for a programmer to communicate with his or her checker.
No no, you're literally ignorant about this. There's a whole industry out there of automated proof checking of code via type theory and type systems and there's technology that enables this. It's just not mainstream. It's more obscure then haskell but it's very real.
It's only unlikely to you because you're completely ignorant about type theory. You're unaware of how "complex" that "language" can get. Dependent types is one example of how that "type language" can actually "type check" your entire program to be not just type correct but logically correct. Lean, Idris, Coq, Agda, literally are technologies that enable proof checking at the type level. It's not unlikely at all. it's reality.
>Please do not hold it against me if I do not continue commenting here - you must be from a different, parallel Universe. (How is Elvis doin' on your end? ;) J/K)
It's quick sort implemented in a language called idris. The implementation is long because not only is it just quick sort, the programmer is utilizing the type system to PROVE that quick sort actually does what it's suppose to do (sort ordinal values).
I'd appreciate an apology if you had any gall. But you likely won't "continue commenting here". Wow just wow. I am holding it against you 100%. I didn't realize how stupid and rude people can actually be.
"Typestates are a technique for moving properties of state (the dynamic information a program is processing) into the type level (the static world that the compiler can check ahead-of-time)."
> you're completely ignorant about type theory. (...) This is just fucking rude. (...) I didn't realize how stupid and rude people can actually be.
Yes, of course, naturally, you must be right, how blind could I have been?
> I'd appreciate an apology if you had any gall.
Sure, sorry about my little previous joke[1], meant no factual offense. The very best of luck to you as a programmer and a wonderfully polite human being with a great sense of humor.
[1] "Topper: I thought I saw Elvis. Block: Let it go, Topper. The King is gone. Let's head for home." ("Hot Shots!", 1991)
>Sure, sorry about my little previous joke[1], meant no factual offense. The very best of luck to you as a programmer and a wonderfully polite human being with a great sense of humor.
Jokes are supposed to be funny. Not offensive. Your intent was offense under the guise of humor. Common tactic. Anyone serious doesn't take well to the other party being sarcastic or joking, you know this, yet you still play games. It's a typical strategy to win the crowd by making someone overly serious look like a fool. But there is no crowd here, nobody is laughing. Just me and you.
So your real intent is just to piss me off given that you know nobody is here to laugh at your stupid joke. Your just a vile human being. Go ahead crack more jokes. Be more sarcastic, it just shows off your character. We're done.
> Your intent was offense (...) you still play games (...) a typical strategy to win the crowd (...) But there is no crowd here (...) your real intent is just to piss me off (...) Your just a vile human being (...) it just shows off your character
I assure you that I am not joking when I say the following: you are beginning to act in a disturbing manner at this point, please consider speaking to a mental health professional.
Again, sorry to have caused you discomfort with my little joke and best of luck to you.
Bro. If someone was truly disturbing and you truly wanted to help them wouldn't walk up to them and tell them to speak to a mental health professional. Telling them that is even more offensive. We both know this.
You're not joking. You're just being an even bigger ass, but now instead of jokes, you're feigning concern. It's stupid.
There's subtle motivations behind everything. A genuine apology comes without insulting the other party. Clearly you didn't do that here, and clearly you and everyone else knows what a genuine apology should NOT look like: "go get help with your mental problems, I'm really sorry."
It shows just what kind of person you are. It's not me who's disturbing... it's you, the person behind a mask.
Also clearly my words are from a place of anger and seriousness not mental issues. Mental problems are a very grave issue and it's a far bigger problem and the symptoms are far more extreme then what's happening here. But you know this. And you're trying to falsely re-frame the situation by disgustingly using mental issues as some kind of tool to discredit the other party. It's just vile.
I don't wish you the best of luck. I think someone like you doesn't deserve it.
SQlite is written in C. It has type checking. Yet people still write unit tests for it. Why? Because type checking is mostly practically inconsequential. All your points don't prove anything. It proves my point.
All the problems you talk about can be solved with more advanced proof based checkers. These systems can literally proof check your entire program to be fully in spec precompile time. It goes far beyond just types. Agda, Idris, Coq, and Microsofts lean have facilities to prove your programs to be fully correct 100% of the time. They exist. But they're not popular. And there's a reason for that.
You say it's paramount to move error detection to compile time. I say, this problem is ALREADY solved, but remains unused because these methods aren't PRACTICAL.