I wrote a blog post about Agda Core! It's a bit long and not very polished, but I'm happy to have it finished (thanks to a long and distraction-free train ride to Swansea).
A weird thing about being 50 is that there are programming languages that I've used regularly for longer than some of the software developers I work with have been alive. I first wrote BASIC code in the 1980s. The first time I wrote an expression evaluator--a fairly standard programming puzzle or homework--was in 1990. I wrote it in Pascal for an undergraduate homework assignment. I first wrote perl in the early 1990s, when it was still perl 4.036 (5.38.2 now). I first wrote java in 1995-ish, when it was still java 1.0 (1.21 now). I first wrote scala, which I still use for most things today, in 2013-ish, when it was still scala 2.8 (3.4.0 now). At various times I've been "fluent" in 8086 assembly, BASIC, C, Pascal, perl, python, java, scala; and passable in LISP/Scheme, Prolog, old school Mathematica, (early days) Objective C, matlab/octave, and R. I've written a few lines of Fortran and more than a few lines of COBOL that I ran in a production system once. I could probably write a bit of Haskell if pressed but for some reason I really dislike its syntax so I've never been enthusiastic about learning it well. I've experimented with Clean, Flix, Curry, Unison, Factor, and Joy and learned bits and pieces of each of those. I'm trying to decide whether I should try learning Idris, Agda, and/or Lean. I'm pretty sure I'm forgetting a few languages. Bit of 6502 assembly long ago. Bit of Unix/Linux shell scripting languages (old enough to have lived and breathed tcsh before switching to bash; I use fish now mostly).
When I say passable: in graduate school I wrote a Prolog interpreter in java (including parsing source code or REPL input), within which I could run the classic examples like append or (very simple) symbolic differentiation/integration. As an undergraduate I wrote a Mathematica program to solve the word recognition problem for context-free formal languages. But I'd need some study time to be able to write these languages again.
I don't know what the hell prompted me to reminisce about programming languages. I hope it doesn't come off as a humblebrag but rather like old guy spinning yarns. I think I've been through so many because I'm never quite happy with any one of them and because I've had a varied career that started when I was pretty young.
I guess I'm also half hoping to find people on here who have similar interests so I'm going to riddle this post with hashtags:
@BoydStephenSmithJr How do you find using Haskell in a work setting? I always feel like I'm under time pressure and don't have as much as I would like to think through a design. I'm never satisfied with my Scala code for that reason and I feel like it'd feel even worse with Haskell since it's so much more concise.
Am not familiar with GMDTT, will have to check that out! So many things to learn 🤯
@abucci This is my second Haskell job and I'm sure things will depend on the organization around you, but I just do the first thing that I can think of that "will work", make it as simple / concrete / specialized as possible until I have something that compiles without warnings, and only then do I let myself generalize / abstract things. Try to stick documentation on all new top-level bindings while my motivation is fresh, and allow myself to rewrite later.
#agda seems to compile with ghc wasm backend with just a bit of modification (remove custom setup & gitrev)! i'm not familiar with agda internals, but as long as it only involves file i/o and doesn't need to spawn processes to do real work, then in principle it shouldn't be hard to get a fully functional agda in browser working :)
Intrinsically typed core (terms + semantics) paired with an elaborator + lexer + parser to generate core terms from an externally defined language instance. With this approach I can write decent error messages. Unfortunately, this means the DSL is external to the tooling of the host language. I can live with that…
We are organizing the FP Dag aka Dutch Functional Programming Day on Friday the 5th of January in Delft. People from neighboring countries are also very welcome to join!
The (soft) registration deadline is on the 22th of December (next Friday), so get your tickets soon!
Does anyone else do #Agda with #Vim without #DeprecatedPython2 ? The main agda-vim plugin doesn't work at all. The tc-0 fork does some things, but mostly emits bytes v str errors. Last time I tried the agda-language-server, I couldn't get it to compile.
I think some tooling will let me put together this evaluate function a lot faster.
The local season for writing MSc thesis project proposal is here and I have formulated a few ideas for students to start from. They are posted in Chalmers' "MSc thesis portal" and linked from here: https://patrikja.owlstown.net/posts/1968-msc-thesis-proposals
In short, if you want to come to Gothenburg and work with #Agda or #Haskell in relation to some of my research interests, do get in touch.
Tomorrow is already the deadline for the third edition of #WITS, the Workshop on the Implementation of Type Systems, colocated with #POPL 2024 in London. The page limit is one page, but just a single-paragraph abstract with an interesting idea for a talk is also very welcome! In particular contributors to #Haskell#OCaml#Rust#Scala#Coq#Lean#Agda#Idris#Cedille#Arend#CoolTT and even #TypeScript are warmly invited to give a talk about their experiences with implementing type systems.
on the other hand, i think a lot of coq/lean enthusiasts think that tactics are the only way to get this kind of interactivity -- writing partial proofs, seeing your forward-derived assumptions alongside your goal -- whereas the agda and twelf proofs demonstrate otherwise. in the twelf case, you don't even need a fancy emacs mode (as long as you're fine with reloading whole files at a time).
maybe it's because agda and twelf are lesser-known proof assistants, and no one thinks you want to write general purpose programs with tactics (...do they?? 😅 ) so no one thinks it would help? but then we have people using copilot/chatgpt/whatever to do "code completion" which is literally this task except it skips the part where the programmer understands anything.
"Concerning computer assisted proofs, it seems to me the main obstacle is user friendliness; if you want this to become a part of the culture of mathematics, that when you submit a paper it includes a computer verification that the paper is correct -- I think this is very unlikely to become a part of the culture of mathematics, but if you want it to -- then, what you need is proof assistants that mathematicians are willing to use, so that it doesn't take 100 times as long to provide that certificate as it does to produce a paper the usual way."
also worth noting the discussion between Lurie, Urs Schreiber, and others in the comments of this post on Mathematics Without Apologies, one of the more epic flame wars in internet history