Hacker News new | ask | show | jobs
by st1x7 1993 days ago
> problems in finance, energy, medicine, etc., that are more correctness-sensitive than performance-sensitive

What does correctness-sensitivity mean in this context and how is it missing from a language like Python for example?

2 comments

It means that the type system is flexible enough to encode specific domain logic in a way that can be verified by the compiler (and therefore always be correct at runtime unless there is a bug in the compiler). Likewise, it means that plainly incorrect domain logic (eg due to a typo) is far less likely to occur than in a Python program. Some of this can be encoded by statically typed languages like C (“the average of an array of floats is a float”) but not all of it (“given a function that maps floats to floats, applying that function to an array of floats returns an array of floats”).

Python of course has none of this (“this average function actually returns the string ‘fix me!’ on some inputs because the programmer forgot to fill in and else branch”). Mypy is a useful tool but it doesn’t stop type-incorrect code from being executed and isn’t as powerful as Haskell. Likewise, the Haskell compiler certainly doesn’t catch everything, but it does completely eliminate many common Python bugs.

There is obviously a “spectrum” since no general purpose language has a truly rigorous type system.

Idris is not rigorous enough?
The compiler and type system allows you to more robustly encode and enforce correctness. Even as someone who's written relatively little Haskell compared to Python, knowing that I can run it and it's not going to break in some weird, unexpected way is a fantastic feeling. If I had to write something that needed to be logically "bulletproof" and correct, I'd feel orders-of-magnitude more comfortable writing it in Haskell/Rust than Python. Python has too much magic, too many ways to do something unchecked, too many ways to work-around some issue. It's too easy to write poor, difficult-to-comprehend/maintain code in Python, at least with Haskell/Rust I can re-factor something and _know_ that I didn't break anything or change any behaviour - the latter especially is straight up not a guarantee I could make with Python in my experience.