"Nicklaus Wirth felt that something more suitable to operating systems and application development was needed so he began work on Modula. This became Modula-2 and would be essentially finalized around 1984 or so."
I really like #kotlin's (and others') approach to nullability, where nothing is nullable by default and you mark something as nullable by adding '?' to the type. And the '?.' syntax is nice too. 'foo: Foo? = ...; foo?.doThing()' is nicer than 'foo: Optional<Foo> = ...; foo.map(|it| it.doThing())', and both are miles better than "everything is always implicitly nullable unless annotated with '@NotNull' #plt
「 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?
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/
I've been learning about Delimited Continuations lately, because I have recently learned that several programming language theory heavyweights, including Oleg Kiselyov, now believe the classic continuation control construct, e.g. "call/cc" in the #Scheme language, were big mistake that make program optimization needlessly difficult, though I don't fully understand why this would be the case. Unfortunately, "call/cc" is encoded in the Scheme language standard, so compiler authors need to come up with work-arrounds -- who knew at the time of the first revision (1975) it would be a bad idea?
Delimited Continuations solve the problems inherent in continuations (again, I don't understand why), and are composable, meaning it is easy to write modular pieces of code using continuations in isolation that can all be made to fit nicely together with a few simple high-order functions.
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.