「 CakeML is a functional programming language and an ecosystem of proofs and tools built around the language. The ecosystem includes a proven-correct compiler that can bootstrap itself 」
CakeML is a functional programming language and an ecosystem of proofs and tools built around the language. The ecosystem includes a proven-correct compiler that can bootstrap itself.
Finally getting around to my new year’s resolution… I’m looking for PhD opportunities! I’m enjoying myself doing professional software dev right now, but I promised myself after my master’s that I’d try going back to academia eventually; this is the year I want to set that up. So I’m wondering if anyone on here knows of anything that's available. :>
Generally I’d love to do work involving programming languages in the broadest sense of the word, but also involving something that's not traditionally PL theory. For example:
Human factors in PL design: learnability, cognitive processing, etc.
Going beyond plain text for programming: graphical languages, alternative ways of storing & editing code (e.g. Unison), etc.
Applying proof assistants / type theories outside of pure mathematics: natural language semantics, experiment design, etc.
Copy (assignment) semantics and/or requiring captured variables be constant/unchanged for function closures will cover 90% of use cases and make call stack management a brazilian times simpler for the compiler/runtime.
I'm currently looking at annotations / decorations to a research programming language to estimate runtime non-asymptotically (i.e. gimme a number) in a simple execution model. I thought there might be (have been) some similar projects, but I'm not really sure where to look. I vaguely remember some work on proving loop bounds (e.g. polyhedrally). Any hints?
It's so rare that anyone remembers about #scala when talking about other #ProgrammingLanguages like #gleam in this particular case. Just happy and surprised 🧐
I feel like I'm missing something obvious. Someone with a better view than me of #PLT: why have mainstream programming languages never developed unit-of-measure typing?
I know there are some libraries for it in various language ecosystems, and iirc F# has some notion of units. Surely other research languages have it. It seems like something you'd want at compile-time.
some notes towards a « #blender for hackers » tutorial series [1]
I think I want to follow the #racket/#plt/#htdp method of restricting blender to subsets of gradually growing "tutorial-specific workshops" (using the "blender apps" feature that allows you to export just a subset of the application), except have the whole tutorial be an interactive text adventure within these restricted subsets of blender, in which you are directed in the use of various tools to "fill in the blanks" of simple scenes, almost like a coloring book, that introduce new features when you enter a revealed message, or the correct number of vertices in a well-topoligized shape, essentially basing each tutorial off of procedural use of a restricted set of standard blender key commands.
so imagine Tutorial 0, where you are presented with a very minimal "edit mode" workspace,; just a viewport, the selection tool, the rotation axis (+ "drag" "zoom" etc), a terminal prompt introducing the tutorial, and some illegible text out yonder. from the very beginning, I would introduce keyboard "a" (for select all) and numpad "del" (which "brings you" to any set of selected, useful for navigation), which brings you to the message "del the magnificent". entering the message into the text prompt then explains orthographic vs. perspective view, and camera rotation (the numpad keys), and you're instructed to essentially "select, del" between a path of vertices, shifting perpspective to reveal messages at each, which entering introduces more vertices and and key commands, gradually building up a vocabulary, quickly introducing the ruler tool, and really focusing from the start how all the gridwork magically "snaps together", effectively giving you a simulataneously 2D and 3D editing experience where everything perfectly lines up geometry if you navigate and edit procedurally, trying to convey to the user that Blender is really this sort of magical "fantasy #art studio" experience where you have all the tools you would in a serious sculpture or plastic arts studio, except everything is (comparatively) easy and free.
[1] (written as fast as possible, sry if its a mess)
I ported @mattmight’s CPS conversion code (https://matt.might.net/articles/cps-conversion/) to #Haskell and after some fighting with the type system, it worked! To make the interpreters work with the Cont monad, I had to remove recursive lets and hence, functions being able to call themselves recursively, but the rest works fine.
The attached images show the conversion of the Fibonacci function into the CPS version.
I wrote the fourth part of my #blog series “Implementing Co, a small programming language with coroutines”. And this time, we add support for channels in Co for inter-coroutine communication. https://abhinavsarkar.net/posts/implementing-co-4/