Hacker GitHub

← All repos

John-Nagle/pasv

View on GitHub ↗ ★ 52 Common Lisp

The Pascal-F Verifier

27 mentions on Hacker News by 1 person: 0 stories, 27 comments · first 2017-01-19 · latest 2026-10-14

Mentions per year 27 mentions · busiest year 2017 (12)
20082026
AllStoriesComments NewestTopOldest
  1. …on the VAX 11/780 I was using back in the early 1980s.) [1] https://github.com/John-Nagle/nqthm [2] https://github.com/John-Nagle/pasv/blob/master/src/work/temp...
    comment by Animats · 2026-10-14 · in The Four Colour Theorem: The first time machines mogged mathematicians
  2. …code under SCCS and built with make, because the LISP part was only part of the whole system. [1] https://github.com/John-Nagle/pasv/tree/master/src/CPC4
    comment by Animats · 2025-11-20 · in The lost cause of the Lisp machines
  3. …a way to eliminate bugs. This leads to excessive formalism. That tendency has to be restrained. [1] https://github.com/John-Nagle/pasv
    comment by Animats · 2025-05-22 · in Benchmarking Crimes Meet Formal Verification
  4. …set theory first, but I didn't realize that back then. [1] https://github.com/John-Nagle/nqthm [2] https://github.com/John-Nagle/pasv/blob/master/src/work/temp... [3] https://github.com/John-Nagle/pasv/blob/master/src/work/temp...
    comment by Animats · 2024-12-17 · in Natural Number Game: build the basic theory of the natural numbers from scratch
  5. …functions. Boyer and Moore didn't like that idea, and I didn't pursue it further. Fun times. [1] https://github.com/John-Nagle/pasv/blob/master/src/work/temp...
    comment by Animats · 2024-10-22 · in One Plus One Equals Two (2006)
  6. …success in this area.[3] [1] https://archive.org/details/manualzilla-id-5928072/page/n3/m... [2] https://github.com/John-Nagle/pasv [3] https://www.microsoft.com/en-us/research/video/programming-w...
    comment by Animats · 2024-05-05 · in Verified Rust for low-level systems code
  7. …It's fun for retro reasons, but things have moved on. [1] https://github.com/John-Nagle/nqthm [2] https://github.com/John-Nagle/pasv/tree/master/src/CPC4
    comment by Animats · 2024-02-14 · in Why is Common Lisp not the most popular programming language?
  8. …https://sites.math.rutgers.edu/~zeilberg/Opinion160.html [2] https://github.com/John-Nagle/nqthm [3] https://github.com/John-Nagle/pasv/blob/master/src/work/temp...
    comment by Animats · 2024-01-19 · in Opinions of Doron Zeilberger
  9. …hate case analysis. Computers are good at it. [1] https://github.com/John-Nagle/nqthm [2] https://github.com/John-Nagle/pasv/blob/master/src/work/temp...
    comment by Animats · 2023-06-30 · in Will Computers Redefine the Roots of Math?
  10. …extreme would be a GUI program. [1] http://www.animats.com/papers/verifier/verifiermanual.pdf [2] https://github.com/John-Nagle/pasv
    comment by Animats · 2023-04-10 · in What I've Learned About Formal Methods in Half a Year
  11. …[2] https://theory.stanford.edu/~arbrad/papers/arrays.pdf [3] https://github.com/John-Nagle/pasv/blob/master/src/work/temp... [4] https://github.com/John-Nagle/nqthm
    comment by Animats · 2022-05-30 · in Grothendieck's Approach to Equality [pdf]
  12. …x=y => f(x)=f(y). Pure functions can safely be used in assertions and conditional debug code. [1] https://github.com/John-Nagle/pasv/blob/master/src/CPC2/p2tr...
    comment by Animats · 2020-05-03 · in The naked truth about writing a programming language (2014)
  13. …here is still having that problem. Good times back then. But we were way ahead of our time. [1] https://github.com/John-Nagle/pasv [2] https://github.com/John-Nagle/nqthm [3] https://github.com/John-Nagle/pasv/blob/master/src/work/temp...
    comment by Animats · 2019-09-09 · in The Future of Mathematics? [pdf]
  14. …[2] http://www.animats.com/papers/verifier/verifiermanual.pdf [3] https://github.com/John-Nagle/pasv [4] https://link.springer.com/content/pdf/10.1007/BFb0026441.pdf
    comment by Animats · 2019-04-16 · in Rust: Beyond the Typechecker
  15. …range and subscript errors. [1] https://www.cs.tau.ac.il/~msagiv/courses/ATP/p245-nelson.pdf [2] https://github.com/John-Nagle/pasv
    comment by Animats · 2019-02-06 · in Programming the Z3 SMT solver
  16. …//docs.microsoft.com/en-us/windows-hardware/drivers/de... [3] https://github.com/John-Nagle/nqthm [4] https://github.com/John-Nagle/pasv
    comment by Animats · 2017-12-24 · in Formal Verification: The Gap Between Perfect Code and Reality
  17. …Remember, it can blow at any seam. It only takes one buffer overflow to allow an exploit. [1] https://github.com/John-Nagle/pasv
    comment by Animats · 2017-09-01 · in Announcing Rust 1.20
  18. …Moore were trying really hard to make the results understandable to traditional mathematicians. [1] https://github.com/John-Nagle/pasv/blob/master/src/work/temp...
    comment by Animats · 2017-07-17 · in What makes maths beautiful?
  19. …complaining that it's too complicated seems whiny. [1] https://github.com/John-Nagle/nqthm [2] https://github.com/John-Nagle/pasv/blob/master/src/work/temp...
    comment by Animats · 2017-07-16 · in What makes maths beautiful?
  20. …and arrows to Unicode line drawing characters. This was a small part of another project. It's here: https://github.com/John-Nagle/pasv/blob/master/src/Util/picf...
    comment by Animats · 2017-06-22 · in Show HN: ShakyDraw – Hand-drawn block diagrams from plain text
  21. …┃ data ┃ ┗━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━┛ [1] https://github.com/John-Nagle/pasv/blob/master/src/Util/picf...
    comment by Animats · 2017-02-24 · in Uber CLI
  22. https://github.com/John-Nagle/pasv/tree/master/src/CPC4
    comment by Animats · 2017-02-08 · in Lisp is not functional (2010)
  23. See the link listed above: https://github.com/John-Nagle/pasv/blob/master/src/CPC4/z.li... I put all the code on Github. The oldest version of each file is exactly what ran in 1986. The code is delicate. It's a theorem prover, and there's…
    comment by Animats · 2017-01-24 · in What Happens When You Mix Java with a 1960 IBM Mainframe
  24. …[2] http://www.softwarepreservation.org/projects/LISP/franz/Fran... [3] https://github.com/John-Nagle/pasv/blob/master/src/CPC4/z.li... [4] https://en.wikipedia.org/wiki/Greg_Nelson_(computer_scientis...
    comment by Animats · 2017-01-23 · in What Happens When You Mix Java with a 1960 IBM Mainframe
  25. …mathematical notation for verification purposes. This is a huge turnoff for programmers. [1] https://github.com/John-Nagle/pasv/blob/master/src/CPC4/defm...
    comment by Animats · 2017-01-20 · in Dafny – A programming language with a program verifier
  26. …has been for a long time. (Having 3000x as much compute power as we had in 1982 helps a lot.) [1] https://github.com/John-Nagle/pasv [2] https://github.com/John-Nagle/pasv/blob/master/src/Examples
    comment by Animats · 2017-01-20 · in Dafny – A programming language with a program verifier
  27. https://github.com/John-Nagle/pasv
    comment by Animats · 2017-01-19 · in Turbo Pascal Compiler (2013)