- Formally Verifying Rust's Opaque Types
- New Coq tutorial
- Rupicola: Relational Compilation for Performance-Critical Applications
- Rupicola: Relational Compilation for Performance-Critical Applications
- Rupicola: Relational Compilation for Performance-Critical Applications
- fiat-crypto: Cryptographic Primitive Code Generation by Fiat
- A dependently-typed proof language intended to make provably correct bare metal code possible for working software engineers.
- A dependently-typed proof language intended to make provably correct bare metal code possible for working software engineers.
- A dependently-typed proof language intended to make provably correct bare metal code possible for working software engineers.
- Make formal verification and provably correct software practical and mainstream
- Make formal verification and provably correct software practical and mainstream
- Hello Letlang! My programming language targeting Rust
- Hey, at risk of making a tired question, I could use a little help with something that I'm finding myself stuck on as an of-two-days proof assistant and Coq user. ∀x : ℕ, 3 | (x + 5x). Specifically, what's got me is showing that ∀x y z : ℕ, (z|x and z|y) -> z|(x + y). Attempt in post body.
- Esoteric Sorting Algorithms
- Ask HN: Can the same individual accomplish more with programming than proofs?
- It took Russell and that other guy 360 pages to prove that 1+1=2. That's how rigorous math is.
- Which is the most abstract and bizzare book of mathematics you have ever came across?
- Who Can Name the Bigger Number?
- The technological case against Bitcoin and blockchain
- The Software Foundations: mathematical underpinnings of reliable software
- Restrict Implementations of a Trait at Compile Time.
- Software can literally be perfect: How Formal Verification and Magmide could make provably correct code tractable for practicing software engineers.
- Lol
- Make provably correct code possible for working software engineers
- Advent of Code Day 1
- Two Mechanisations of WebAssembly 1.0
- Type Theory Forall Podcast #13 - C/C++, Emacs, Haskell, and Coq. The Journey (John Wiegley)
- Shell sort
- Or even built-in libraries
- Whitehead and Russell’s Principia rewritten in Coq
- Whitehead and Russell’s Principia rewritten in Coq
- The Principia Rewrite: Whitehead and Russell’s Principia Rewritten in Coq
- My Path to Magma
- There's an ongoing effort to rewrite Principia Mathematica using Coq
- Writing a Fuzzer for NES Games
- Magma: A Dependently-Typed Language
- Orion 0.17 – X25519 with formally-verified field arithemtic and serde support
- The 50-year-old problem that eludes theoretical computer science
- Orion 0.17 - X25519 with formally-verified field arithemtic and serde support
- Math Foundations from Scratch
- Binary GCD
- Multicore OCaml: September 2021, effect handlers will be in OCaml 5.0
- Coverage Is Not Strongly Correlated with Test Suite Effectiveness
- What are real world examples of dependent types signficant improving security or productivity?
- Proof Assistant Makes Jump to Big-League Math | Quanta Magazine
- A Proven Correct C Compiler (Used by Airbus)
- CompCert C a formally verified optimizing compiler for a large subset of C99
- Solution to the four color theorem in haskell