Hacker News new | ask | show | jobs
by repiret 33 days ago
My experience is that there's a correlation between powerful type systems and the property that once your program compiles, it's correct. Compiles == correct is rarely true in C or JavaScript. It's often true in Haskell and Rust. TypeScript is somewhere in between C and Rust.

There's a niche available for a language which is relatively easy for a human to read, but with a very powerful at the expense of difficult to use type system. The language would let you make all sorts of assertions whose meaning are easy for the human to see, but to compile would need to come along with correctness proofs. The language is meant to be written by AI, which can battle the compiler, and write the proofs, but then read by humans who can verify that the AI wrote the program they wanted and/or direct the AI to make changes.
1 comments
munksbeer 33 days ago
>My experience is that there's a correlation between powerful type systems and the property that once your program compiles, it's correct. Compiles == correct is rarely true in C or JavaScript. It's often true in Haskell and Rust.

I find this staggeringly hard to believe. Most bugs are logic errors. How does Rust or Haskell prevent these?

link
mightybyte 32 days ago
Haskell gives you quite a powerful set of tools for constraining and reasoning about your program's behavior. For instance, its ability to define pure functions and control side effects is a very powerful tool for preventing certain classes of bugs. Dereferencing invalid pointer locations and out of bounds array lookups are large classes of bugs in mainstream languages that Haskell basically eliminates entirely. It's not at all the same thing as what you get from the type systems in languages like Java, C++, etc. You really have to try it to appreciate it.
link
yakshaving_jgt 33 days ago
> Most bugs are logic errors.

Are they? IME most bugs are type errors.

Or rather, IME most bugs are logic errors only because I've excluded the possibility of type errors by using a sophisticated type system.

link
munksbeer 33 days ago
Most of my bugs are logic errors. I write Java. Your comment seems to imply that moving to Rust or Haskell would make a correct program if it compiles.
link
yakshaving_jgt 33 days ago
I don't think porting your program to Haskell would make your program correct.

I think porting your program to Haskell would make all of your bugs logic errors, rather than only most of them.

link