Elektrine lite

← Feed

Jacques Carette

JacquesC2@types.pl

<p>Computing Scientist, ex-mathematician. Currently in academia, spent considerable time in industry as well. Into weird programming languages and the outer parts of programming and software engineering. Currently exploring metaprogramming, quantum programming, DSLs and &quot;generate everything&quot;.</p>

Posts

  • View post

    When even the abstract is complete nonsense. Sigh.

  • View post

    Listening to a bunch of Bee Gee&#39;s stuff right now. My, they were so good! Yes, I like them. And Lorna Shore and Rammstein and Rush and Metric and Abba and Avril Lavigne and The Hu and Nusrat Fateh Ali Khan. And so many more.

  • View post

    I think I like doing work with a proof assistant for exactly the reason that drove others nuts: there is nowhere for tacit knowledge to hide. I was reminded of this while trying to read some &quot;paper math&quot; on type theoretical forcing. I can&#39;t just click on some bits to ask &quot;what exactly do you mean by this part here&quot;. [The thing I wanted to know was indeed never defined, just assumed to be known.]

  • View post

    It would be hilarious if what un-scaled university classes (i.e. pushed them to be smaller) was LLMs. If a class is supposed to be teaching students some skills, then we can no longer check if that has been successful &quot;remotely&quot; (i.e. via written assignments). So we have to check them in-person. Which takes a lot more time.

  • View post

    Hard puzzle: what do Perth, Scotland and Erfoud, Morocco have in common? [Answer might be delayed, wifi connection where I am is not necessarily good.]

  • View post

    Now this is the kind of software engineering research that I&#39;d like to see more of! https://arxiv.org/abs/2602.10540

  • View post

    @egbertrijke I quite like formalizations that are made to look like encyclopedia pages. I just dislike when they are made to serve double-duty, i.e. serve a narrative purpose as well as a &quot;source code for a library&quot; purpose at the same time. Then you&#39;re forced into all sorts of compromises. Libraries need vastly different organization than good narrative does. I don&#39;t actually care which one ends up being the primary artifact. [But my current best guess is that it&#39;s eas...

  • View post

    &quot;We present a sorry-free formalization&quot; -- as if a document with &#39;sorry&#39;s in them could be called a formalization?

  • View post

    When I agreed to be on the PC for conference X, I did not think I had agreed to review alchemy papers. And yet, here we are. Yes, this is about &quot;modern AI&quot;.

  • View post

    &quot;Never hallucinate or make anything up.&quot; Sounds like instructions for the orange one at trial. Or instructions a reporter might wish to give before an interview.

  • View post

    github crumbling because of AI is both sad and funny. And annoying: can&#39;t do my code reviews right now.

  • View post

    Damn. I jotted down a quick idea in my research notes file (in markdown, in github, using the web edit function). Copilot auto-filled a commit message as a starting point. It was good. That is super annoying.

  • View post

    I&#39;d love it if there was a tradition of putting in an &quot;author&#39;s version&quot; of a paper onto the arxiv. No, I don&#39;t mean the extended version, I mean the version with all the puns, side stories, footnotes and the like kept in. And sure, the proofs too.

  • View post

    This is the point of formalization: In several places, the process of formalization sharpened our understanding of the informal presentation. p. 4 of a just-landed formalization of the reals in cubical agda. https://users.cs.utah.edu/~blg/resources/pdf/jackson-brough-cubicalreals-2026.pdf

  • View post

    No one who has done enough proving should ever say that a &quot;program has been proven correct.&quot; Does it satisfy the theorems you&#39;ve proven? Sure. Are they all the theorems needed to say &#39;correct&#39;? Extremely unlikely!