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 Lean in production, then their approach is compelling.

The idea is that you start with a Lean specification, create a fully verified implementation with respect to the spec, and then hook it and the production implementation up to a fuzzer or source or random inputs. Then you can explore a lot of the state space fully automatically.

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 rephrase the sentence.

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 hygienic procedural macros), and the focus on supporting professional mathematicians gives a different feel to the community and libraries. I think both are worth knowing, but either is great to learn. I hope the two projects learn more from each other in the future.

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 for dumping the source to Pandoc's dialect of Markdown, from which I was going to generate those, but the differences in Markdown dialects are enough that it was a fair bit of work.

Dropping a print version and focusing on epub could very well be faster, as I suspect that an mdbook->epub pipeline is less challenging than creating a quality print-ready PDF. But no plans right now.

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'd like to get back into it once I'm recovered a bit.

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 dependent types with Software Foundations and Coq, and that was very helpful when learning Agda and Idris later. Similarly, skills from them transferred quite readily to Lean.

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. It's intended to be accessible to Python, C#, Rust, Kotlin, Java, TypeScript, and Scala developers. Today marks the final release, after more than a year of writing.

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 machine precommits to an encryption of its count (e.g. by printing some paper with evidence on it), and then the voter decides whether to spoil the ballot or actually cast it. If the voter spoils the ballot, then they get a new paper ballot to vote on, but they can retain the commitment. Voters may spoil any number of ballots. Decryptions of spoiled ballots along with enough information to check the machine's work are provided to the voter, either immediately or at the end of the day. This means that a cheating machine cannot cheat very much, though the whole thing also really relies on a verifiable privacy-preserving audit trail for the actual count (e.g. with homomorphic encryption). It at least means that nobody need trust the actual computers.

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... .