#rocq — Public Fediverse posts
Live and recent posts from across the Fediverse tagged #rocq, aggregated by home.social.
-
Is anyone going here this weekend? Agda is one of the most innovative game changers in functional programming and theorem proving, given its unique implementation architecture and capabilities. I'd like to meet you there! π🐫λ #CubicalAgda #Rocq #OCaml #Haskell types2026.cse.chalmers.se
TYPES 2026: TYPES 2026 -
Coq theorem prover is now called Rocq
#HackerNews #Coq #Rocq #theorem #prover #programming #languages #proof #assistants
-
Readings shared December 5, 2025. https://jaalonso.github.io/vestigium/posts/2025/12/06-readings_shared_12-05-25 #ATP #Autoformalization #DataScience #FunctionalProgramming #Haskell #ITP #LeanProver #Math #Rocq #Rstats #SMT #Z3
-
Readings shared November 7, 2025. https://jaalonso.github.io/vestigium/posts/2025/11/08-readings_shared_11-07-25 #AI #Agda #AlphaEvolve #FormalVerification #FunctionalProgramming #Haskell #HoTT #ITP #LLM #LeanProver #Math #Rocq
-
I've been thinking about something that's related to Tarski's undefinability theorem (and might possibly be a corollary if viewed from the right angle), but relates to computability rather than truth. It seems to have implications for systems like Agda and Rocq, which I don't have much experience with, but which I think will (at least with certain settings) only let you define computable things. I'd love to know if this is well-known already.
Suppose you have a system, S, that lets you encode (as natural numbers) definitions of computable functions from Nat to Bool. Not every natural number has to represent such a function, but given any natural number, n, you have to be able to tell whether n is the encoding of such a function, and if it is, you have to be able to evaluate it for any natural number you want.
Now we can define a function f that takes a natural number n as input, and returns a boolean value which is True if and only if n is the encoding (in S) of a computable function g from Nat to Bool, and g(n) = False.
By the constraints I described for S, this must be a computable function. So can it be encoded in S?
No! If it could be encoded as a natural number k, then f(k) would be True if and only if f(k) = False.
So Agda, for example, with settings that allow only definitions of computable things, can't allow definitions of all computable functions. In particular, it seems it can't implement a complete simulation of Agda with the same settings.
This is almost the opposite of the problem with the halting problem. A universal Turing machine can simulate a universal Turing machine, but it can't always tell if it will halt if given certain input. Agda can guarantee that any algorithm you write in it will halt, but, if my reasoning above is correct, it can't simulate itself.
So what other computable functions might not be definable in Agda? What obstacles would you find, for example, if you tried to simulate Agda in Agda?
-
I seem to remember some compiled-to-html output of proof scripts (could have been either #Rocq, #Isabelle or #Lean, but maybe also a different proof assistant) which let you see the type of subterms on hover. Does this ring a bell w anyone? (I certainly wish we had sth like this for #Agda, my current approach is to replace the respective term w a hole and then reload the file and `C-c C-d` which is obviously not static, not to mention computationally expensive…)
