Is Haskell a good choice for software security?

Re:Is Haskell a good choice for software security? by whateveracct on Friday December 17, 2021 @05:45PM (#29599276)

  data Void where
    Void :: { absurd :: forall a. a } -> Void

^ I just defined a type with no inhabitants [1] along with the ability to use a value of it to prove anything. And it leans on the type system features & ergonomics Go & Rust don't even get close to having.

This is a pedantic example in a way, but this type is actually very useful in practice! And defining the type almost reads like English (or at least math English.)

Haskell is just a different world. You program with type variables of different shapes and sizes and relationships like it's nothing and it Just Works. Go's new generics & Rust's are crufty in comparison. Both due to syntax and semantics.

[1] modulo bottom..I know, I know :)

[ Parent | on HN ]

Re:Is Haskell a good choice for software security? by juxtapose on Saturday December 18, 2021 @01:09AM (#29602154)

> modulo bottom

Since GHC 9.2, with UnliftedDatatypes you can define real uninhabited types!

    {-# LANGUAGE UnliftedDatatypes #-}
    import GHC.Exts
    data Void :: TYPE UnliftedRep where
      Void :: { absurd :: forall a. a } -> Void

[ Parent | on HN ]

Re:Is Haskell a good choice for software security? by whateveracct on Saturday December 18, 2021 @02:41PM (#29607838)

Resplendent!

[ Parent | on HN ]