https://github.com/cucapra/dahlia
A language + a Compiler written in Scala for High-Level Synthesis (FPGA programming).
A language + a Compiler written in Scala for High-Level Synthesis (FPGA programming).
GitHub
GitHub - cucapra/dahlia: Time-sensitive affine types for predictable hardware generation
Time-sensitive affine types for predictable hardware generation - cucapra/dahlia
🔥1
Refocusing Programming Languages Theory from programs to programming: http://tomasp.net/histogram/
Tomas Petricek presents and discusses (at length!) a prototype of a new programming language (together with two interactive online editors!) built around the process of constructing a program, not the end artifact. The language named Histogram encapsulates a formal interaction calculus representing several user interactions with a system that result in a (partial) program.
As Tomas points out this approach is akin to interactive theorem proving with tactics, where the user interacts with the system writing down tactics which implicitly build a program (most often a formal proof is a (kind of) program).
But explicit focus on interactions allows going further and capturing not only usual notions of programs-as-texts or programs-as-ASTs, but also such atypical (in academic research) forms as Jupyter Notebooks with heavily non-linear (in reality) evaluation order and implicit global state of computation. Plus good old autocompletion. 😊
The fun part: we can develop a type system for interaction calculus with non-trivial metatheoretic and practical properties. Rephrasing Robin Milner's "Well-typed programs cannot go wrong" — "Well-typed interactions cannot produce ill-typed programs". 😁
Tomas Petricek presents and discusses (at length!) a prototype of a new programming language (together with two interactive online editors!) built around the process of constructing a program, not the end artifact. The language named Histogram encapsulates a formal interaction calculus representing several user interactions with a system that result in a (partial) program.
As Tomas points out this approach is akin to interactive theorem proving with tactics, where the user interacts with the system writing down tactics which implicitly build a program (most often a formal proof is a (kind of) program).
But explicit focus on interactions allows going further and capturing not only usual notions of programs-as-texts or programs-as-ASTs, but also such atypical (in academic research) forms as Jupyter Notebooks with heavily non-linear (in reality) evaluation order and implicit global state of computation. Plus good old autocompletion. 😊
The fun part: we can develop a type system for interaction calculus with non-trivial metatheoretic and practical properties. Rephrasing Robin Milner's "Well-typed programs cannot go wrong" — "Well-typed interactions cannot produce ill-typed programs". 😁
tomasp.net
Histogram: You have to know the past to understand the present
To invent new programming tools, we need to shift our focus from programs to programming. Programs are created through a variety of interactions, but programming research often forgets about those. In this interactive essay, we represent programs as lists…
👍4🔥3
https://unsound-workshop.org/
A workshop at SPLASH 2022 about unsoundness in specifications, systems or expectations. CFP is open till 2022-09-01 (but no formal publication).
Expecting lots of Rust folks. 😁
A workshop at SPLASH 2022 about unsoundness in specifications, systems or expectations. CFP is open till 2022-09-01 (but no formal publication).
Expecting lots of Rust folks. 😁
👍2😁1
Образцово-показательный проект на "современном JavaScript": https://github.com/lukeed/preact-progress
Один (sic!) файл исходников и два (sic!!!) файла конфигурации системы сборки. Это они ещё
Если вы думаете, что это единственный такой проект — посмотрите по Гитхабу повнимательнее.
Один (sic!) файл исходников и два (sic!!!) файла конфигурации системы сборки. Это они ещё
package-lock.json не закоммитили и нет отдельного конфига для Babel.Если вы думаете, что это единственный такой проект — посмотрите по Гитхабу повнимательнее.
GitHub
GitHub - lukeed/preact-progress: Simple and lightweight (~590 bytes gzip) progress bar component for Preact
Simple and lightweight (~590 bytes gzip) progress bar component for Preact - GitHub - lukeed/preact-progress: Simple and lightweight (~590 bytes gzip) progress bar component for Preact
🥱4💩1
Кто катит в кубер по утрам
Тот поступает мудро!
Известно всем, парам-парам,
На то оно и утро!
Скучна вечерняя пора,
Девопсеры зевают.
Но если катим мы с утра
Такого не бывает!
Тот поступает мудро!
Известно всем, парам-парам,
На то оно и утро!
Скучна вечерняя пора,
Девопсеры зевают.
Но если катим мы с утра
Такого не бывает!
👍2
"time-series of image data" — а я всегда думал, что это называется видео... 🤔
😁6🤯2
https://www.youtube.com/channel/UCzipicZiZ1843jAqmSGgYwg
Video recordings of talks from "50 years of Smalltalk". It has a talk on theorem proving... 🤔
Video recordings of talks from "50 years of Smalltalk". It has a talk on theorem proving... 🤔
👍1
https://www.youtube.com/watch?v=Iz70bD63RWY
Looks neat... If they really manage to turn it into a TV-show... 😏
Looks neat... If they really manage to turn it into a TV-show... 😏
YouTube
Infinity System Trailer
Infinity System is a scifi western tv show where all may not be as it seems.
To find out more visit wolfpackentertainment.co/projects or Instagram @wolfpackentertainment.co
To find out more visit wolfpackentertainment.co/projects or Instagram @wolfpackentertainment.co
https://news.ycombinator.com/item?id=11941656
Under the linked message advertising Luna language (now Enso) there's a thread between Alan Kay and Rich Hickey concerning "Data vs. Objects".
The most immediately striking thing is that Rich is much more thoughtful and deep than he seems! 😅
Adding to the discussion, I guess the fact (a datum?! 🤔) that we can decipher ancient languages for which we have no interpreters around for millennia to large extend might hint that (structured) data is indeed kinda more fundamental than objects...
Under the linked message advertising Luna language (now Enso) there's a thread between Alan Kay and Rich Hickey concerning "Data vs. Objects".
The most immediately striking thing is that Rich is much more thoughtful and deep than he seems! 😅
Adding to the discussion, I guess the fact (a datum?! 🤔) that we can decipher ancient languages for which we have no interpreters around for millennia to large extend might hint that (structured) data is indeed kinda more fundamental than objects...
http://aitp-conference.org/2022/
Apparently, there's an annual conference on all things AI and Mechanised Theorem Proving (automatic, interactive and their integration). Topics cover everything from mining archives of formal proofs to proving correctness of ML algorithms to AGI applications.
This year's speaker lineup is insane from Ben Goertzel and Stephen Wolfram to Kevin Buzzard and Talia Ringer.
Apparently, there's an annual conference on all things AI and Mechanised Theorem Proving (automatic, interactive and their integration). Topics cover everything from mining archives of formal proofs to proving correctness of ML algorithms to AGI applications.
This year's speaker lineup is insane from Ben Goertzel and Stephen Wolfram to Kevin Buzzard and Talia Ringer.
For those who still doesn't follow closely Lawrence Paulson's blog (shame on you!) he reviews Turing Machines, some other equivalent formalisms and the history of their development: https://lawrencecpaulson.github.io/2022/07/06/Turing_Machines.html
🔥2
https://www.youtube.com/watch?v=ou4xmq4C7uI
Для низкобюджетного "домашнего" проекта — удивительно хорошо!
Для низкобюджетного "домашнего" проекта — удивительно хорошо!
YouTube
BLACK MARKET BRAWL - An Action Short Film
Turbo Action Presents:
BLACK MARKET BRAWL
A Treasure-Hunting Mercenary and a Black Market Salesman attempt to sell an ancient artefact: A ring that gives it's barer “god-like” powers. Shit hits the fan when the ring is revealed to be missing right as the…
BLACK MARKET BRAWL
A Treasure-Hunting Mercenary and a Black Market Salesman attempt to sell an ancient artefact: A ring that gives it's barer “god-like” powers. Shit hits the fan when the ring is revealed to be missing right as the…
https://blog.brownplt.org/2022/06/28/static-python.html
> This work focuses on the Static Python language built by the Instagram team at Meta.
🧐
> In particular, we find that the design holds up the intent of soundness well, but the act of modeling it uncovered several bugs (including one that produced a segmentation fault), all of which have now been fixed.
🤔
> As an aside, this paper is a collaboration that was born entirely thanks to Twitter and most probably would never have occurred withtout it.
😁
> This work focuses on the Static Python language built by the Instagram team at Meta.
🧐
> In particular, we find that the design holds up the intent of soundness well, but the act of modeling it uncovered several bugs (including one that produced a segmentation fault), all of which have now been fixed.
🤔
> As an aside, this paper is a collaboration that was born entirely thanks to Twitter and most probably would never have occurred withtout it.
😁
blog.brownplt.org
Gradual Soundness: Lessons from Static Python
👍1
https://arrdem.com/2022/07/04/superficial_simplicity/
A reflection on "Simple Made Easy", "Growing a Language", macros and complexity management. Points out (once again) the tension between user-extensibility and tool-analysability.
A reflection on "Simple Made Easy", "Growing a Language", macros and complexity management. Points out (once again) the tension between user-extensibility and tool-analysability.
https://github.com/readme/featured/functional-programming
«Functional programming is finally going mainstream»
Well, if GitHub themselves say so then who are we to disagree?
«Functional programming is finally going mainstream»
Well, if GitHub themselves say so then who are we to disagree?
GitHub
Functional programming is finally going mainstream
With origins that stretch back to the late 1950s, functional programming might seem dated—but it can be a boon for growing teams working with large codebases. Read more from @klintron:
👍3
https://nickchk.com/causalgraphs.html
Causal inference! With animations! 😄
The post explains and illustrates basic notions and methods of causal inference with examples from econometrics. And animated plots, yep.
#causalinference #statistics
Causal inference! With animations! 😄
The post explains and illustrates basic notions and methods of causal inference with examples from econometrics. And animated plots, yep.
#causalinference #statistics
👍1
https://medium.com/@Reisen_0/a-review-of-the-case-against-education-bacc120cb8cd
A very interesting and thoughtful piece on Human Capital vs. Signalling in Education. Pretty fascinating topic, many academic references, great read.
A very interesting and thoughtful piece on Human Capital vs. Signalling in Education. Pretty fascinating topic, many academic references, great read.
Medium
A Review of “The Case Against Education”
This is a lightly edited repost of a twitter thread. So, short paragraphs ahoy:
https://imgur.com/a/rnATR7D
A flowchart guiding a regression model construction out of bunch of variables. Touches subtle causal issues.
#statistics #datascience
A flowchart guiding a regression model construction out of bunch of variables. Touches subtle causal issues.
#statistics #datascience
Imgur
A Flowchart for Constructing a Regression Model
Post with 1582 views. A Flowchart for Constructing a Regression Model
https://nickch-k.github.io/DataVizChecklist/
A concise "obvious" but totally useful #data #visualization #checklist
Actually I'd say it does not emphasize enough the need for a meaningful story before you try to visualize it. And if you're preparing visualization for an academic publication does not emphasize enough the importance of large enough readable titles and captions. 😄
A concise "obvious" but totally useful #data #visualization #checklist
Actually I'd say it does not emphasize enough the need for a meaningful story before you try to visualize it. And if you're preparing visualization for an academic publication does not emphasize enough the importance of large enough readable titles and captions. 😄
DataVizChecklist
Data Visualization Checklist
A brief checklist to go through before you’re done with your data visualization, or as you’re using it.