Hacker News
José A. AlonsoReadings shared June 5, 2026. https://jaalonso.github.io/vestigium/posts/2026/06/05-readings_shared_06-05-26 #AI4Math #Agda #Autoformalization #CoqProver #FunctionalProgramming #Haskell #ITP #IsabelleHOL #LeanProver #Logic #Math #RacketLang
A computational toolkit for engagement and scalable assessment in a large Logic course. ~ Stephen M. Watt. https://arxiv.org/abs/2606.02367v1 #Logic #RacketLang
A Computational Toolkit for Engagement and Scalable Assessment in a Large Logic Course
Large required courses in theoretical computer science face two related challenges: helping students engage with abstract material and supporting reliable student assessment at scale. This paper describes LogicLab, a lightweight computational toolkit developed for CS 245, Logic and Computation, at the University of Waterloo. The course is required for undergraduate computer science students and serves a large annual cohort. The main pedagogical objective is to help students concretize the ideas they encounter in lectures and assignments. Handwritten formulas and proof steps do not give students immediate correctness feedback. This can slow their development of confidence in formal reasoning and makes assessment harder to apply consistently at scale. LogicLab addresses this by allowing students to manipulate formulas, transformations, clauses, valuations, and proof steps as computational objects in Racket, building directly on their Scheme/Racket experience from the first-year curriculum. LogicLab provides tools for parsing and displaying formulas, applying equivalence transformations, converting to normal forms, simplifying formulas, working with valuations, applying resolution rules, running a Davis-Putnam style procedure, and verifying formal deduction steps. The system is lighter than a general proof assistant such as Coq or Lean and uses notation aligned with the course. It exposes composable functions students can invoke individually or use to program their own automations. The paper presents the design rationale, system organization, and planned course integration of LogicLab as a practical model for using computational tools to support engagement, conceptual concreteness, and more consistent assessment in large formalreasoning courses.
soapdog#LuaLang is probably my fav imperative language and #RacketLang or #SchemeLang my fav functional one. Can't decide between Racket and Scheme, I want to like Scheme more but I have much more experience with Racket.
R7RS Large has seen a new release and now #SchemeLang has nested defines.
I was reading it and was like, wasn’t that there forever? Then I remembered I been programming in #RacketLang 😹😹😹
I was reading it and was like, wasn’t that there forever? Then I remembered I been programming in #RacketLang 😹😹😹
jbz∆ Lisp: Common Lisp, Racket, Clojure, Emacs Lisp - Hyperpolyglot https://hyperpolyglot.org/lisp
Jacquelineif there's one thing I miss in documentation systems other than Scribble (for #racketlang), it's the ability to designate arbitrary words and phrases as "technical terms" and turn uses of those terms into links to a place in the docs where you've defined the term
all hail @tech{} and @deftech{}
wrote about some #racketlang ideas I had for an automated planning language
Sketching a planning language
Sketching a planning language
RacketRacket meet-up: Saturday, 7 March 2026 at 18:00 UTC
EVERYONE WELCOME 😁
Announcement, Jitsi Meet link & discussion at https://racket.discourse.group/t/racket-meet-up-saturday-7-march-2026/4128
unhinged #racketlang idea: `raco diff-test`
run it on a PR or commit, and like how `raco test` finds and runs `test` submodules, it finds and runs `diff-test` submodules
diff tests would be able to test things about the commit, like that files A and B are always modified together