Hacker News new | ask | show | jobs
by exdsq 1602 days ago
I've worked on commercial Haskell projects and it was actually quite nice! Tooling was a pain, libraries may be lacking, but describing a complex domain as a state machine in the type system with automatically generated tests (via properties) and formal methods to prove some of the core algorithms was a really interesting way to develop. Not sure it'd be my pick for my own startup though.
1 comments
nextos 1602 days ago
What formal methods did you use?
link
exdsq 1602 days ago
Combination of Agda, Isabelle, Coq, and TLA+ depending on the team - I mostly interacted with TLA+ and the compiled Haskell from Agda specs :)
link
dwohnitmok 1602 days ago
Wow definitely want to pick your brain. How large/# of LOC were the Agda, Isabelle, and Coq specs? What industry was this?
link
exdsq 1602 days ago
Blockchain - two repos with specs are:

* https://github.com/input-output-hk/cardano-ledger

* https://github.com/input-output-hk/plutus

There's quite a few recent Isabelle repos such as https://github.com/input-output-hk/high-assurance-legacy

link