hwayne/lets-prove-leftpad
View on GitHub ↗ ★ 758 SystemVerilog
Proving leftpad correct two-dozen different ways
9 mentions on Hacker News by 6 people: 4 stories, 5 comments · first 2020-02-14 · latest 2025-11-03
20082026
-
…[1] http://concrete-semantics.org [2] https://github.com/lean-forward/logical_verification_2025 [3] https://github.com/hwayne/lets-prove-leftpad
comment by nextos · 2025-11-03 · in Why don't you use dependent types? -
…you want to use String and StringBuilder to do the padding, which arguably be more idiomatic. [1] https://github.com/hwayne/lets-prove-leftpad/blob/ea9c0f09a2... [2] https://docs.oracle.com/en/java/javase/25/docs/api//java.bas... [3]…
comment by marginalia_nu · 2025-10-15 · in Breaking "provably correct" Leftpad -
…of proofs of leftpad in different prover languages, so people can compare them. It's here: https://github.com/hwayne/lets-prove-leftpad [/invalid closing tag]
comment by hwayne · 2024-06-12 · in Terence Tao on proof checkers and AI programs -
…Haskell community" My experience is that other refinement type systems are way less complex. See: https://github.com/hwayne/lets-prove-leftpad In particular, compare https://github.com/hwayne/lets-prove-leftpad/blob/master/liq... to…
comment by nextos · 2022-10-16 · in Simon Peyton Jones interview -
…code correct via inline JML annotations. [1]: https://amturing.acm.org/vp/clarke_1167964.cfm [2]: https://github.com/hwayne/lets-prove-leftpad
comment by hwayne · 2020-02-14 · in The Business Case for Formal Methods