Suguivy@ekaitz_zarraga ohh, proof assistants are tools for proving properties about programs, theorem, etc., but machine-checked, so you can be 100% sure of the correctness. They are usually (or at least the ones I'm interested in) based in a type theory (like lambda calculus) and in the Curry-Howard corresponce, which is an equivalence between programs (in functional programming) and proofs. For me it's very interesting but these days I don't have many time to deep more :(
Chirp! is a GNU Social instance for the Cooley and Sekula families and their friends.
Chirp! is a social network. It runs on GNU social, version 2.0.1-beta0, available under the GNU Affero General Public License.
All Chirp! content and data are available under the Creative Commons Attribution 3.0 license.