-
Bertie – A minimal, high-assurance implementation of TLS 1.3 written in hacspec
-
Stalin Sort Algorithm
-
So you think you know C?
-
Kami: A Platform for Hardware Specification and Verification
-
bfcoq: Brainfuck compiler in Coq
-
Bfcoq: Brainfuck Compiler in Coq
-
Can the language of proof assistants be used for general purpose programming?
-
Arm’s Cortex A510: Two Kids in a Trench Coat
-
A Taste of Coq and Correct Code by Construction
-
RISC-V CPU formal specification F# edition
-
Languages on the rise like Rust and Go are being quite vocal against inheritance and many engineers seem to agree. Is this the end of inheritance? What do you think?
-
Will Computers Redefine the Roots of Math?
-
Dilemma: very unhappy with a highly-paying tech job. What to do?
-
Which proof assistant is the best to formalize real analysis/probability/statistics?
-
Basics of Proofs [pdf]
-
All??
-
Recently I am having too much friction with the borrow checker... Would you recommend I rewrite the compiler in another language, or keep trying to implement it in rust?
-
Discussion Thread
-
Inspiring OOP examples?
-
I’ve seen a trend of many right wingers in paradox games so let’s see if that’s true
-
Announcing Magmide Month! (proof language for/using Rust)
-
Relationship between category theory and HoTt?
-
There is such thing called bugfree code.
-
Proofs about Programs
-
Is "my version" of quick-sort incorrect?
-
AI Language Models Are Struggling to “Get” Math
-
What are some possible research questions on compiler construction
-
Is it possible to make C as safe as Rust?
-
Aneris: Program logic for developing and verifying distributed systems
-
What is the need of formally verified compilers? Where are they used? Do verified compiler support all features that unverified compiler do?
-
I made repository containing the sorting and searching algorithms a developer must know
-
Development Environment with guix shell for Coq Package
-
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.
-
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.