Conversation

Notices

1. Embed this notice
   someodd (someodd@fosstodon.org)'s status on Sunday, 01-Dec-2024 06:46:30 JST someodd

   Why #Haskell ? Thread.

   It's such a different way of thinking fundamentally due to the alfonzo/turing split and this has lead to unique features that slowly bleed into the general language ecosystem. One of my favorite features of Haskell is exactness and correctness. The type system lends itself to not just catching the kind of errors that would be normally runtime errors in some other languages, but it it also lends itself to things like formal verification and proof assistants like...

   • alcinnz repeated this.
   • Embed this notice
     someodd (someodd@fosstodon.org)'s status on Sunday, 01-Dec-2024 06:46:28 JST someodd

     in reply to

     In this code above is I actually "verify" important properties of the important thing: file ranking works as expected.

     It's explicitly NOT "if I give x input I get y output" style unit test. The "statistical verification" comes from the fact that you can programmatically generate inputs and verify the outputs, and thus generate >1,000 test "cases" from just one actual property test.

     And this is because, I think, you're dealing with more abstract logic, which Haskell really lends itself to.

   • Embed this notice
     screwlisp (screwtape@mastodon.sdf.org)'s status on Sunday, 01-Dec-2024 06:46:28 JST screwlisp

     in reply to

     @someodd what do you think of all the prior lazy and formal work in lisp (or like, testing if you must) compared to Haskell's later developments?

     I got really into Lisp's Series[1] recently, since I found it just generated a better fizzbuzz than I manually wrote myself in my initial test.

     [1]https://dspace.mit.edu/bitstream/handle/1721.1/6035/AIM-1082.pdf?sequence=2&isAllowed=y

   • Embed this notice
     someodd (someodd@fosstodon.org)'s status on Sunday, 01-Dec-2024 06:46:29 JST someodd

     in reply to

     ... #LiquidHaskell (restriction types, SMT solver) and the Isabelle proof assistant.

     For example, look at the kind of assurances we can make about data at the type-level. This means the SMT solver can assure that certain logical constraints on types are provably true.

     My code to verify a file ranking algo I made:

     https://github.com/someodd/bore/blob/master/src/Bore/SpacecookieClone/Search/Verified.hs

     alcinnz repeated this.
   • Embed this notice
     someodd (someodd@fosstodon.org)'s status on Sunday, 01-Dec-2024 06:46:29 JST someodd

     in reply to

     But also, I think Haskell was maybe one of the first places you saw property testing, and I think it's kind of the norm in this ecosystem. Just look at a unique way of thinking testing *properties* rather than just "dumb" unit tests are:

     https://github.com/someodd/bore/blob/master/test/Spec.hs

     What's happening here is a kind of statistical verification of *properties* that should prove true about the actual entrypoint/main functions that *do the thing*...

   • Embed this notice
     prozacchiwawa (prozacchiwawa@functional.cafe)'s status on Sunday, 01-Dec-2024 14:29:11 JST prozacchiwawa

     in reply to

     @someodd haskell's base type system is pretty expressive even without liquid haskell. sandy maguire's book "thinking in types" really opened my eyes to what kind of computation was achievable at the normal type level in haskell.