Coq Posts

Latest Coq related posts with mentions of open-source projects
  • Translation of the Rust's core and alloc crates to Coq for formal verification

    3 projects | news.ycombinator.com | about 1 month ago
  • Proving with Coq the 5th Busy Beaver number, BB(5)=47,176,870

    1 project | news.ycombinator.com | about 1 month ago
  • Bertie – A minimal, high-assurance implementation of TLS 1.3 written in hacspec

    5 projects | news.ycombinator.com | 3 months ago
  • Stalin Sort Algorithm

    1 project | news.ycombinator.com | 4 months ago
  • So you think you know C?

    2 projects | news.ycombinator.com | 5 months ago
  • Kami: A Platform for Hardware Specification and Verification

    1 project | news.ycombinator.com | 6 months ago
  • bfcoq: Brainfuck compiler in Coq

    1 project | /r/programming | 6 months ago
  • Bfcoq: Brainfuck Compiler in Coq

    1 project | news.ycombinator.com | 7 months ago
  • Can the language of proof assistants be used for general purpose programming?

    3 projects | news.ycombinator.com | 8 months ago
  • Arm’s Cortex A510: Two Kids in a Trench Coat

    1 project | news.ycombinator.com | 9 months ago
  • A Taste of Coq and Correct Code by Construction

    3 projects | news.ycombinator.com | 10 months ago
  • RISC-V CPU formal specification F# edition

    6 projects | news.ycombinator.com | 11 months ago
  • 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?

    2 projects | /r/rust | 12 months ago
  • Will Computers Redefine the Roots of Math?

    6 projects | news.ycombinator.com | 12 months ago
  • Dilemma: very unhappy with a highly-paying tech job. What to do?

    1 project | /r/cscareerquestionsuk | 12 months ago
  • Which proof assistant is the best to formalize real analysis/probability/statistics?

    3 projects | /r/Coq | 12 months ago
  • Basics of Proofs [pdf]

    1 project | news.ycombinator.com | 12 months ago
  • All??

    2 projects | /r/ProgrammerHumor | about 1 year ago
  • 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?

    1 project | /r/programmingcirclejerk | about 1 year ago
  • Discussion Thread

    2 projects | /r/neoliberal | over 1 year ago
  • Inspiring OOP examples?

    1 project | /r/java | over 1 year ago
  • I’ve seen a trend of many right wingers in paradox games so let’s see if that’s true

    1 project | /r/ParadoxExtra | over 1 year ago
  • Announcing Magmide Month! (proof language for/using Rust)

    1 project | /r/rust | over 1 year ago
  • Relationship between category theory and HoTt?

    1 project | /r/math | over 1 year ago
  • There is such thing called bugfree code.

    1 project | /r/ProgrammerHumor | over 1 year ago
  • Proofs about Programs

    1 project | news.ycombinator.com | over 1 year ago
  • Is "my version" of quick-sort incorrect?

    1 project | /r/learnprogramming | over 1 year ago
  • AI Language Models Are Struggling to “Get” Math

    1 project | news.ycombinator.com | over 1 year ago
  • What are some possible research questions on compiler construction

    1 project | /r/Compilers | over 1 year ago
  • Is it possible to make C as safe as Rust?

    3 projects | /r/C_Programming | over 1 year ago
  • Aneris: Program logic for developing and verifying distributed systems

    1 project | news.ycombinator.com | over 1 year ago
  • What is the need of formally verified compilers? Where are they used? Do verified compiler support all features that unverified compiler do?

    1 project | /r/compsci | over 1 year ago
  • I made repository containing the sorting and searching algorithms a developer must know

    2 projects | /r/dotnet | almost 2 years ago
  • Development Environment with guix shell for Coq Package

    1 project | /r/GUIX | almost 2 years ago
  • Formally Verifying Rust's Opaque Types

    2 projects | news.ycombinator.com | almost 2 years ago
  • New Coq tutorial

    3 projects | /r/ProgrammingLanguages | almost 2 years ago
  • Rupicola: Relational Compilation for Performance-Critical Applications

    1 project | /r/Compilers | almost 2 years ago
  • Rupicola: Relational Compilation for Performance-Critical Applications

    1 project | /r/ProgrammingLanguages | almost 2 years ago
  • Rupicola: Relational Compilation for Performance-Critical Applications

    1 project | news.ycombinator.com | almost 2 years ago
  • fiat-crypto: Cryptographic Primitive Code Generation by Fiat

    1 project | news.ycombinator.com | almost 2 years ago
  • A dependently-typed proof language intended to make provably correct bare metal code possible for working software engineers.

    1 project | /r/programming | about 2 years ago
  • A dependently-typed proof language intended to make provably correct bare metal code possible for working software engineers.

    1 project | /r/coding | about 2 years ago
  • A dependently-typed proof language intended to make provably correct bare metal code possible for working software engineers.

    1 project | /r/compsci | about 2 years ago
  • A dependently-typed proof language intended to make provably correct bare metal code possible for working software engineers.

    1 project | /r/Coq | about 2 years ago
  • A dependently-typed proof language intended to make provably correct bare metal code possible for working software engineers.

    1 project | /r/ProgrammingLanguages | about 2 years ago
  • Make formal verification and provably correct software practical and mainstream

    1 project | /r/patient_hackernews | about 2 years ago
  • Make formal verification and provably correct software practical and mainstream

    1 project | /r/hackernews | about 2 years ago
  • Hello Letlang! My programming language targeting Rust

    2 projects | /r/rust | about 2 years ago
  • 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.

    1 project | /r/Coq | about 2 years ago
  • Esoteric Sorting Algorithms

    3 projects | dev.to | about 2 years ago