d_christiansen

6 ms·

1. 1.▲
   by d_christiansen 7mo ago

   Cedar ( https://lean-lang.org/use-cases/cedar/ ) at AWS use an executable Lean model of a system as an oracle for differential testing of a Rust implementation. If you can't run Lean in production, then their a
2. 2.▲
   by d_christiansen 7mo ago

   In Lean, strings are packed arrays of bytes, encoded as UTF-8. Lean is very careful about performance; after all, a self-hosted system that can't generate fast code would not scale.
3. 3.▲
   by d_christiansen 3y ago

   I agree - this is inelegant. I'll make an issue in the repo to rephrase this sentence for the next time I do a round of typo fixes. Thanks for the feedback!
4. 4.▲
   by d_christiansen 3y ago

   I'm the author - I think that it's good to signal this kind of thing redundantly, and not rely on the details of typesetting to avoid confusion. I'll create an issue in the repo to rephrase the sentence.
5. 5.▲
   by d_christiansen 3y ago

   Thank you! I hope you enjoy the rest of it.
6. 6.▲
   by d_christiansen 3y ago

   Lean occupies a different point in the design space. Its type theory is simpler and more conservative, its metaprogramming system is more reminiscent of Racket's (including hygienic procedural macros), and the focus on supporting profe
7. 7.▲
   by d_christiansen 3y ago

   Unfortunately not. I wanted to produce PDF and epub versions in parallel with the HTML version, but getting those to be of sufficient quality would have blown the time budget for the project. There's some old code in the Git history fo
8. 8.▲
   by d_christiansen 3y ago

   Thank you for reading it, and I hope that the final chapter is also enjoyable for you. Right now, I plan to take a break - this book occupied every Saturday for about a year, and some time off is in order. But Lean is tons of fun, and I&#x2
9. 9.▲
   by d_christiansen 3y ago

   Thanks! I hope you find it valuable! Those other languages are also definitely worth learning. Happily, there's lots of cross-transfer of ideas and skills between them, so learning one will make the others easier. I got my start in dep
10. 10.▲
    by d_christiansen 3y ago

    Lean 4 is an interactive theorem prover. It's also a programming language with a self-hosting compiler. This is a free book on using Lean 4 as a programming language, written without assuming any background in functional programming. I
11. 11.▲
    Functional Programming in Lean(leanprover.github.io)

    159 points by d_christiansen 3y ago|37 comments
12. 12.▲
    by d_christiansen 4y ago

    Another nice method to reduce risk from electronic counting is called the "Benaloh Challenge" (after Josh Benaloh, the inventor). The idea is that there are two steps to putting the paper ballot into the machine: first, the machin
13. 13.▲
    by d_christiansen 4y ago

    Thanks for the links! If Haskell is more your style than Racket, there's a Haskell version of the implementation tutorial at https://davidchristiansen.dk/tutorials/implementing-types-hs... .
14. 14.▲
    Functional Programming in Lean – an in-progress book(leanprover.github.io)

    2 points by d_christiansen 4y ago|0 comments