Lingolol

José A. AlonsoReadings shared July 18, 2025. <a href="https://jaalonso.github.io/vestigium/posts/2025/07/19-readings_shared_07-18-25" rel="nofollow noopener" translate="no" target="_blank">https://jaalonso.github.io/vestigium/posts/2025/07/19-readings_shared_07-18-25</a> <a href="https://mathstodon.xyz/tags/ACL2" class="mention hashtag" rel="nofollow noopener" target="_blank">#ACL2</a> <a href="https://mathstodon.xyz/tags/CompSci" class="mention hashtag" rel="nofollow noopener" target="_blank">#CompSci</a> <a href="https://mathstodon.xyz/tags/FunctionalProgramming" class="mention hashtag" rel="nofollow noopener" target="_blank">#FunctionalProgramming</a> <a href="https://mathstodon.xyz/tags/Haskell" class="mention hashtag" rel="nofollow noopener" target="_blank">#Haskell</a> <a href="https://mathstodon.xyz/tags/ITP" class="mention hashtag" rel="nofollow noopener" target="_blank">#ITP</a> <a href="https://mathstodon.xyz/tags/LLMs" class="mention hashtag" rel="nofollow noopener" target="_blank">#LLMs</a> <a href="https://mathstodon.xyz/tags/LeanProver" class="mention hashtag" rel="nofollow noopener" target="_blank">#LeanProver</a> <a href="https://mathstodon.xyz/tags/Rocq" class="mention hashtag" rel="nofollow noopener" target="_blank">#Rocq</a> <a href="https://mathstodon.xyz/tags/Rust" class="mention hashtag" rel="nofollow noopener" target="_blank">#Rust</a> <a href="https://mathstodon.xyz/tags/Teaching" class="mention hashtag" rel="nofollow noopener" target="_blank">#Teaching</a>

José A. AlonsoTeaching software specification (Experience report). ~ Cameron Moy, Daniel Patterson. <a href="https://ccs.neu.edu/~camoy/pub/lsl.pdf" rel="nofollow noopener" translate="no" target="_blank">https://ccs.neu.edu/~camoy/pub/lsl.pdf</a> <a href="https://mathstodon.xyz/tags/CompSci" class="mention hashtag" rel="nofollow noopener" target="_blank">#CompSci</a> <a href="https://mathstodon.xyz/tags/Teaching" class="mention hashtag" rel="nofollow noopener" target="_blank">#Teaching</a> <a href="https://mathstodon.xyz/tags/ITP" class="mention hashtag" rel="nofollow noopener" target="_blank">#ITP</a> <a href="https://mathstodon.xyz/tags/LeanProver" class="mention hashtag" rel="nofollow noopener" target="_blank">#LeanProver</a> <a href="https://mathstodon.xyz/tags/ACL2" class="mention hashtag" rel="nofollow noopener" target="_blank">#ACL2</a>

José A. AlonsoCSLib: An open-source Lean 4 library formalizing a significant subsetof undergraduate-level computer science. ~ Clark Barrett et als. <a href="https://docs.google.com/presentation/d/1aJFM3EaI4LcppHR_2YFQHiBjUfMMhMKxCeM3BfINi48" rel="nofollow noopener" translate="no" target="_blank">https://docs.google.com/presentation/d/1aJFM3EaI4LcppHR_2YFQHiBjUfMMhMKxCeM3BfINi48</a> <a href="https://mathstodon.xyz/tags/ITP" class="mention hashtag" rel="nofollow noopener" target="_blank">#ITP</a> <a href="https://mathstodon.xyz/tags/LeanProver" class="mention hashtag" rel="nofollow noopener" target="_blank">#LeanProver</a> <a href="https://mathstodon.xyz/tags/CompSci" class="mention hashtag" rel="nofollow noopener" target="_blank">#CompSci</a>

José A. Alonso<a href="https://mathstodon.xyz/tags/MULCIA" class="mention hashtag" rel="nofollow noopener" target="_blank">#MULCIA</a>: Applied researcher in formal methods (Lean4) at Axiomatic_AI. <a href="https://tinyurl.com/ylsqbu6e" rel="nofollow noopener" translate="no" target="_blank">https://tinyurl.com/ylsqbu6e</a> <a href="https://mathstodon.xyz/tags/Jobs" class="mention hashtag" rel="nofollow noopener" target="_blank">#Jobs</a> <a href="https://mathstodon.xyz/tags/CompSci" class="mention hashtag" rel="nofollow noopener" target="_blank">#CompSci</a> <a href="https://mathstodon.xyz/tags/LeanProver" class="mention hashtag" rel="nofollow noopener" target="_blank">#LeanProver</a>

Joshua GrochowHas anyone played around with encouraging (but not requiring) students to teach one another?One way of demonstrating mastery of the material is teaching it to others. I feel like if student A says "Student B really helped me understand the material" that increases my Bayesian posterior that student B understood the material really well (and also that student A understood it, since presumably after student B explained it, student A understood it at least better than they did before).I wouldn't do this as the only, or even major, part of their grade, but it seems like if the grade is to reflect learning, that teaching it to others certainly reflects on their learning.(Additional context: this is for a university-level elective technical course in Comp Sci, for 3rd and 4th-years mostly. I generally do flipped classroom and alternative grading - some combo of ungrading, mastery-based, standards-based, but I'm open to ideas. The class has about 55 students, so whatever it is can take some time but not be *too* time-intensive on me & the one TA.)<a href="https://mathstodon.xyz/tags/AlternativeGrading" class="mention hashtag" rel="nofollow noopener" target="_blank">#AlternativeGrading</a> <a href="https://mathstodon.xyz/tags/grading" class="mention hashtag" rel="nofollow noopener" target="_blank">#grading</a> <a href="https://mathstodon.xyz/tags/teaching" class="mention hashtag" rel="nofollow noopener" target="_blank">#teaching</a> <a href="https://mathstodon.xyz/tags/education" class="mention hashtag" rel="nofollow noopener" target="_blank">#education</a> <a href="https://mathstodon.xyz/tags/CSEd" class="mention hashtag" rel="nofollow noopener" target="_blank">#CSEd</a> <a href="https://mathstodon.xyz/tags/ComputerScience" class="mention hashtag" rel="nofollow noopener" target="_blank">#ComputerScience</a> <a href="https://mathstodon.xyz/tags/CompSci" class="mention hashtag" rel="nofollow noopener" target="_blank">#CompSci</a>

José A. Alonso<a href="https://mathstodon.xyz/tags/MULCIA" class="mention hashtag" rel="nofollow noopener" target="_blank">#MULCIA</a>: Doctoral/Postdoctoral Position in Formal Methods and Verification, Konstanz (Germany). <a href="https://tinyurl.com/ysyqy3g5" rel="nofollow noopener" translate="no" target="_blank">https://tinyurl.com/ysyqy3g5</a> <a href="https://mathstodon.xyz/tags/PhD" class="mention hashtag" rel="nofollow noopener" target="_blank">#PhD</a> <a href="https://mathstodon.xyz/tags/PostDoc" class="mention hashtag" rel="nofollow noopener" target="_blank">#PostDoc</a> <a href="https://mathstodon.xyz/tags/CompSci" class="mention hashtag" rel="nofollow noopener" target="_blank">#CompSci</a>

José A. Alonso<a href="https://mathstodon.xyz/tags/MULCIA" class="mention hashtag" rel="nofollow noopener" target="_blank">#MULCIA</a>: 2 Postdoc Positions in Homotopy Type Theory, University of Nottingham (UK). <a href="https://tinyurl.com/ysld3f5r" rel="nofollow noopener" translate="no" target="_blank">https://tinyurl.com/ysld3f5r</a> <a href="https://mathstodon.xyz/tags/PostDoc" class="mention hashtag" rel="nofollow noopener" target="_blank">#PostDoc</a> <a href="https://mathstodon.xyz/tags/CompSci" class="mention hashtag" rel="nofollow noopener" target="_blank">#CompSci</a>

José A. Alonso<a href="https://mathstodon.xyz/tags/MULCIA" class="mention hashtag" rel="nofollow noopener" target="_blank">#MULCIA</a>: PhD positions in formal methods and planning, Gothenburg (Sweden) <a href="https://tinyurl.com/ywa5vee6" rel="nofollow noopener" translate="no" target="_blank">https://tinyurl.com/ywa5vee6</a> <a href="https://mathstodon.xyz/tags/PhD" class="mention hashtag" rel="nofollow noopener" target="_blank">#PhD</a> <a href="https://mathstodon.xyz/tags/CompSci" class="mention hashtag" rel="nofollow noopener" target="_blank">#CompSci</a>

cst1<a href="https://a.gup.pe/u/academicchatter" class="u-url mention" rel="nofollow noopener" target="_blank">@academicchatter</a> Okay, what tools would you recommend using to help order, browse, visualize and expand your research library? I'm using Zotero as the backing library manager + <a href="https://researchrabbitapp.com/" rel="nofollow noopener" translate="no" target="_blank">https://researchrabbitapp.com/</a> for the visualization/discovery part but open to suggestions and tips!<a href="https://chaos.social/tags/academia" class="mention hashtag" rel="nofollow noopener" target="_blank">#academia</a> <a href="https://chaos.social/tags/phd" class="mention hashtag" rel="nofollow noopener" target="_blank">#phd</a> <a href="https://chaos.social/tags/research" class="mention hashtag" rel="nofollow noopener" target="_blank">#research</a> <a href="https://chaos.social/tags/compsci" class="mention hashtag" rel="nofollow noopener" target="_blank">#compsci</a>

José A. Alonso<a href="https://mathstodon.xyz/tags/MULCIA" class="mention hashtag" rel="nofollow noopener" target="_blank">#MULCIA</a>: Two postdoctoral positions in homotopy type theory at the University of Nottingham, UK. <a href="https://tinyurl.com/ysld3f5r" rel="nofollow noopener" translate="no" target="_blank">https://tinyurl.com/ysld3f5r</a> <a href="https://mathstodon.xyz/tags/PostDoc" class="mention hashtag" rel="nofollow noopener" target="_blank">#PostDoc</a> <a href="https://mathstodon.xyz/tags/CompSci" class="mention hashtag" rel="nofollow noopener" target="_blank">#CompSci</a>

Papers We Love📜 A Byzantine Fault Tolerant Distributed Commit Protocol [2007]By: Wenbing Zhao📖 <a href="https://github.com/papers-we-love/papers-we-love/blob/master/distributed_systems/byzantine-fault-tolerant-distributed-commit-protocol.pdf" rel="nofollow noopener" translate="no" target="_blank">https://github.com/papers-we-love/papers-we-love/blob/master/distributed_systems/byzantine-fault-tolerant-distributed-commit-protocol.pdf</a> 🔍 <a href="https://www.semanticscholar.org/paper/ebb685399ffe65d1b3119ada60fdf002cfac66f9" rel="nofollow noopener" translate="no" target="_blank">https://www.semanticscholar.org/paper/ebb685399ffe65d1b3119ada60fdf002cfac66f9</a><a href="https://mstdn.io/tags/semanticScholar" class="mention hashtag" rel="nofollow noopener" target="_blank">#semanticScholar</a> <a href="https://mstdn.io/tags/paperswelove" class="mention hashtag" rel="nofollow noopener" target="_blank">#paperswelove</a> <a href="https://mstdn.io/tags/research" class="mention hashtag" rel="nofollow noopener" target="_blank">#research</a> <a href="https://mstdn.io/tags/compsci" class="mention hashtag" rel="nofollow noopener" target="_blank">#compsci</a>

José A. AlonsoReadings shared June 30, 2025. <a href="https://jaalonso.github.io/vestigium/posts/2025/07/01-readings_shared_07-01-25" rel="nofollow noopener" translate="no" target="_blank">https://jaalonso.github.io/vestigium/posts/2025/07/01-readings_shared_07-01-25</a> <a href="https://mathstodon.xyz/tags/CompSci" class="mention hashtag" rel="nofollow noopener" target="_blank">#CompSci</a> <a href="https://mathstodon.xyz/tags/FunctionalProgramming" class="mention hashtag" rel="nofollow noopener" target="_blank">#FunctionalProgramming</a> <a href="https://mathstodon.xyz/tags/Haskell" class="mention hashtag" rel="nofollow noopener" target="_blank">#Haskell</a> <a href="https://mathstodon.xyz/tags/ITP" class="mention hashtag" rel="nofollow noopener" target="_blank">#ITP</a> <a href="https://mathstodon.xyz/tags/IsabelleHOL" class="mention hashtag" rel="nofollow noopener" target="_blank">#IsabelleHOL</a> <a href="https://mathstodon.xyz/tags/Logic" class="mention hashtag" rel="nofollow noopener" target="_blank">#Logic</a> <a href="https://mathstodon.xyz/tags/Maxima" class="mention hashtag" rel="nofollow noopener" target="_blank">#Maxima</a> <a href="https://mathstodon.xyz/tags/Teaching" class="mention hashtag" rel="nofollow noopener" target="_blank">#Teaching</a>

José A. AlonsoTeaching children thinking. ~ Seymour A. Papert (1971). <a href="https://citejournal.org/volume-5/issue-3-05/seminal-articles/teaching-children-thinking" rel="nofollow noopener" translate="no" target="_blank">https://citejournal.org/volume-5/issue-3-05/seminal-articles/teaching-children-thinking</a> <a href="https://mathstodon.xyz/tags/CompSci" class="mention hashtag" rel="nofollow noopener" target="_blank">#CompSci</a> <a href="https://mathstodon.xyz/tags/Teaching" class="mention hashtag" rel="nofollow noopener" target="_blank">#Teaching</a>

Aether~Fedi, I have a <a href="https://plasmatrap.com/tags/ComputerScience" rel="nofollow noopener" target="_blank">#ComputerScience</a> (maybe <a href="https://plasmatrap.com/tags/Linguistics" rel="nofollow noopener" target="_blank">#Linguistics</a> ?) Question I need your lovely guidance for ❤️:boosts_ok_gay:💙 I have a design problem about grammar ambiguity ish stuff and want to find reading, resources or theory I can check out to get a good understanding of the problem space. Particularly, I'm trying to find different techniques to use when a given word can appear in multiple parts of the syntax, in order to reduce ambiguity. I'm being deliberately vague because I'm trying to think about generalisable heuristics here, but here's an example of the type of problems I'm thinking about. Sorry it's computery: You have two strings (or lists of tokens) you want to combine into a single string, separated by a delimiter, such that both strings can be retrieved again. But, that delimiter can show up in either of the two strings. What are the ways you can sanitize the input strings or format the final string to clarify where one string ends and the other begins, and how do various restrictions in the input strings affect those precautions? Possible techniques I've thought of are: - designate an escape token and prepend all instances of the delimiter within the strings with it (eg <code>\"</code>) (which is pretty universally used nowadays) - when the delimiter appears in the string, put a repeat copy of it to distinguish it from the delimiter. e.g. <code>"this string contains "" one quote mark"</code> - Another crazy option would be interlacing the two strings so all even tokens belong to string 1 and odd ones are string 2. You'd have length difference issues, but maybe there are other solutions taking a similar thought process. So yeah I'm looking for stuff like that so I can figure out good patterns for unambiguous yet elegant grammars. For a tad more context, I'm thinking about command line argument formats, trying to think of the most user friendly ways one can handle complex data as a list of arguments. Also please boost and let me know if there's hashtags I should include etc :ablobcatheart: <a href="https://plasmatrap.com/tags/CompSci" rel="nofollow noopener" target="_blank">#CompSci</a> <a href="https://plasmatrap.com/tags/programming" rel="nofollow noopener" target="_blank">#programming</a> <a href="https://plasmatrap.com/tags/askfedi" rel="nofollow noopener" target="_blank">#askfedi</a> <a href="https://plasmatrap.com/tags/TechSupport" rel="nofollow noopener" target="_blank">#TechSupport</a>

José A. AlonsoReadings shared June 27, 2025. <a href="https://jaalonso.github.io/vestigium/posts/2025/06/28-readings_shared_06-27-25" rel="nofollow noopener" translate="no" target="_blank">https://jaalonso.github.io/vestigium/posts/2025/06/28-readings_shared_06-27-25</a> <a href="https://mathstodon.xyz/tags/AI" class="mention hashtag" rel="nofollow noopener" target="_blank">#AI</a> <a href="https://mathstodon.xyz/tags/AI4Math" class="mention hashtag" rel="nofollow noopener" target="_blank">#AI4Math</a> <a href="https://mathstodon.xyz/tags/Autoformalization" class="mention hashtag" rel="nofollow noopener" target="_blank">#Autoformalization</a> <a href="https://mathstodon.xyz/tags/CategoryTheory" class="mention hashtag" rel="nofollow noopener" target="_blank">#CategoryTheory</a> <a href="https://mathstodon.xyz/tags/CompSci" class="mention hashtag" rel="nofollow noopener" target="_blank">#CompSci</a> <a href="https://mathstodon.xyz/tags/ITP" class="mention hashtag" rel="nofollow noopener" target="_blank">#ITP</a> <a href="https://mathstodon.xyz/tags/LLMs" class="mention hashtag" rel="nofollow noopener" target="_blank">#LLMs</a> <a href="https://mathstodon.xyz/tags/LeanProver" class="mention hashtag" rel="nofollow noopener" target="_blank">#LeanProver</a> <a href="https://mathstodon.xyz/tags/Math" class="mention hashtag" rel="nofollow noopener" target="_blank">#Math</a> <a href="https://mathstodon.xyz/tags/Mizar" class="mention hashtag" rel="nofollow noopener" target="_blank">#Mizar</a>

Papers We Love📜 A New Approach to Linear Filtering and Prediction Problems [2001]By: T. Başar📖 <a href="https://github.com/papers-we-love/papers-we-love/blob/master/data_fusion/a-new-approach-to-linear-filtering-and-prediction-problems.pdf" rel="nofollow noopener" translate="no" target="_blank">https://github.com/papers-we-love/papers-we-love/blob/master/data_fusion/a-new-approach-to-linear-filtering-and-prediction-problems.pdf</a> 🔍 <a href="https://www.semanticscholar.org/paper/d36a38125557764efb0fd2b3ef0a4cde515b3861" rel="nofollow noopener" translate="no" target="_blank">https://www.semanticscholar.org/paper/d36a38125557764efb0fd2b3ef0a4cde515b3861</a><a href="https://mstdn.io/tags/semanticScholar" class="mention hashtag" rel="nofollow noopener" target="_blank">#semanticScholar</a> <a href="https://mstdn.io/tags/paperswelove" class="mention hashtag" rel="nofollow noopener" target="_blank">#paperswelove</a> <a href="https://mstdn.io/tags/research" class="mention hashtag" rel="nofollow noopener" target="_blank">#research</a> <a href="https://mstdn.io/tags/compsci" class="mention hashtag" rel="nofollow noopener" target="_blank">#compsci</a>

vruzDirect WASM→DOM access doesn't leave JavaScript behind - JS could use the same fast path! We could even build Fagnani's exact templating API as a reference implementation on top of it. But unlike a JS-only solution, the platform stays open for potentially superior approaches in ANY language. Rust might build something faster. Zig might build something smaller. That's the kind of competition through collaboration that drives innovation. Everybody wins wins wins. <a href="https://mstdn.social/tags/compsci" class="mention hashtag" rel="nofollow noopener" target="_blank">#compsci</a> <a href="https://mstdn.social/tags/webdev" class="mention hashtag" rel="nofollow noopener" target="_blank">#webdev</a> <a href="https://mstdn.social/tags/wasm" class="mention hashtag" rel="nofollow noopener" target="_blank">#wasm</a> <a href="https://mstdn.social/tags/javascript" class="mention hashtag" rel="nofollow noopener" target="_blank">#javascript</a>

vruzWeb's superpower is its openness. Native JS templating makes JS more ergonomic. Direct WASM→DOM makes the web more OPEN. Which better serves the platform's future? The web shouldn't privilege one language. True platform evolution means equal access to core capabilities for all languages. That's how we get the next generation of web innovation. <a href="https://mstdn.social/tags/compsci" class="mention hashtag" rel="nofollow noopener" target="_blank">#compsci</a> <a href="https://mstdn.social/tags/webdev" class="mention hashtag" rel="nofollow noopener" target="_blank">#webdev</a> <a href="https://mstdn.social/tags/webstandards" class="mention hashtag" rel="nofollow noopener" target="_blank">#webstandards</a> <a href="https://mstdn.social/tags/opensource" class="mention hashtag" rel="nofollow noopener" target="_blank">#opensource</a>

vruzInstead of standardizing one templating syntax (that'll be bikeshedded to death), give us the primitive: fast DOM access from any language. Let a thousand templating libraries bloom - in any language. Lower-level primitives enable more innovation than high-level APIs. That's the Unix philosophy. Simple, composable, powerful. Build the foundation right. <a href="https://mstdn.social/tags/compsci" class="mention hashtag" rel="nofollow noopener" target="_blank">#compsci</a> <a href="https://mstdn.social/tags/webdev" class="mention hashtag" rel="nofollow noopener" target="_blank">#webdev</a> <a href="https://mstdn.social/tags/wasm" class="mention hashtag" rel="nofollow noopener" target="_blank">#wasm</a> <a href="https://mstdn.social/tags/frontend" class="mention hashtag" rel="nofollow noopener" target="_blank">#frontend</a> <a href="https://mstdn.social/tags/unix" class="mention hashtag" rel="nofollow noopener" target="_blank">#unix</a>

vruzFrameworks already solved templating. They're good at it! What they CAN'T solve is the JS monopoly on DOM access. Open that up and watch innovation explode across the entire ecosystem. React, Vue, Svelte - they all work great. But imagine what could be built if any language had direct DOM access. New paradigms, new approaches, new frameworks we can't even conceive of yet. <a href="https://mstdn.social/tags/compsci" class="mention hashtag" rel="nofollow noopener" target="_blank">#compsci</a> <a href="https://mstdn.social/tags/webdev" class="mention hashtag" rel="nofollow noopener" target="_blank">#webdev</a> <a href="https://mstdn.social/tags/javascript" class="mention hashtag" rel="nofollow noopener" target="_blank">#javascript</a>

Recent searches

Search options

Administered by:

Server stats:

#compsci