Viewing profile — d_christiansen

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 Le…

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…

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!

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…

Thank you! I hope you enjoy the rest of it.

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 hygieni…

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 t…

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 s…

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…

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 witho…

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 th…

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-typ…