The author writes:
> "This is the web site for a textbook about practical engineering with the Coq proof assistant. The focus is on building programs with proofs of correctness, using dependent types and scripted proof automation.
> "I'm following an unusual philosophy in this book, so it may ...
Stories by kragen
Bicicleta needs incremental recomputation, like a spreadsheet, to be reasonably efficient. And I just discovered that *ten years ago* this guy Umut Acar (and Guy Blelloch, et al.) found a super rigorous way to derive statically-type-safe incremental versions of non-incremental (i.e. batch) algorithm...
For a few years now I've been sort of hoping that linear logic, other substructural logics, category theory, denotational semantics, and functional reactive programming would sort of make their way into my brain via osmosis. So far this has failed, and this paper (which unfortunately seems to requir...
An FPGA development workflow for FPGA programming without any dirty proprietary software has been a long-sought-after goal for lots of us free-software hackers. Clifford Wolf has finally made it happen, just in the last few months! His [Project IceStorm](http://www.clifford.at/icestorm/) uses his re...
So, this is sort of a talk by Matthew Hammer introducing people to incremental computation, based on his doctoral work under kind of Umut Acar (the self-adjusting computaiton guy) but extending it to avoid recomputation in many more situations, by using partial ordering constraints on the computatio...
Uncle Bob says you shouldn't TDD your test support code, you shouldn't TDD your software's interactions with the physical world, and you shouldn't TDD the things that you just have to fiddle around with until you get them right, such as CSS (and, I suppose, gameplay). This is significant because he'...
Some notes on how to build web apps with no, or minimal, server code.
C\. Scott Ananian explains some fundamental and other possibly fixable reasons Rust is slow: hidden indirection, unnecessary type-system mandated copying, ownership types, and so on.