Programming Languages, Martials Arts and Computers. The Weblog of Chris Double.
I've been reading the book Building High Integrity Applications with Spark to learn more about the [SPARK/Ada](https://en.wikipedia.org/wiki/SPARK_(programming_language)) language for formal verification. It's a great book that goes through lots of examples of how to do proofs in Spark. I wrote a post on Spark/Ada earlier this year and tried some of the examples in the GNAT edition. While working through... more →
This post covers using the latest version of ATS, ATS 2, and goes through proving some basic algorithms. I've written a couple of posts before on using proofs in ATS 1: more →
The ATS programming language has a powerful type and proof system to enable safe construction of programs. Sometimes there is a need to cast a value from one type to another. ATS provides a feature that enables the programming to write their own rules specifying what can be cast. This becomes important when converting types from non-dependent typed values to... more →
A few years ago I wrote a mailing list post on cross compiling ATS to Android. With ATS2 being released the ability to cross compile has been made easier. In this post I'll show how to produce static linux binaries using musl libc and how to build Android and Windows ATS programs by cross compiling on linux. For these examples... more →
I wrote about ZeroNet a few years ago when it was released and it mostly was about decentralized websites. In the time between then and now it has gained a lot of features and regular use. It still does distributed websites well but it adds features suchs as support for sharing large files, merging sites and distributed pseudo-anonymous identity. This... more →