← Back to context

Comment by anyfoo

2 hours ago

Can you produce those studies? Genuinely interested. Intuitively, I would have thought properly used Haskell prevents a lot of bugs by virtue if its type system, which allows for encoding internal constraints to a certain degree.

The extreme end of this is dependent types, which is so strong that it can be used as a foundation for mathematics itself, and is the principle that the Lean, the proof assistance, is used on. A Lean "program" is effectively proven to be bug-free.