> Answering the question raised at the end of Part 1, we take a look at how a hypothetical Strict Haskell would tie the compilers hands despite pervasive purity. We also examine how laziness permits optimizations that come with no intrinsic cost and compare its benefits to a strict language with opt-in laziness. > > Part 1: > > • Laziness in Haskell — Part 1: Prologue > Series Playlist: > > • Laziness in Haskell > > — > Contact: > • Tweag Website: https://www.tweag.io/ > • Tweag Twitter: https://twitter.com/tweagio > • Alexis King's Twitter: https://twitter.com/lexi_lambda

> In the second webinar from our Hackathon series, Fabian Bormann provides an intro into building on Cardano including a list of tools to support you. Next, Mateusz Czeladka discusses how to harness the power of smart contracts with Aiken. > > Click the link below to learn more and to register for the Cardano Summit Hackathon. > https://summit.cardano.org/hackathon/

> We teach you Haskell

> In the past few years, we witnessed the development of multiple smart contract languages - Solidity, Viper, Michelson, Scilla etc. These languages need to enable developers to write correct, predictable behavior smart contract code. Each language development effort therefore ends up spending resources into building formal verification toolsets, compilers, debuggers and other developer tools. > In this episode, we are joined by Grigore Rosu, Professor of computer science at UIUC [University of Illinois at Urbana-Champaign] for a deep dive into the K framework. The K framework is mathematic logic and language that enables language developers to formally define all programming languages; such as C, Solidity and JavaScript. Once a language is formally specified in the K framework, the framework automatically outputs a range of formal verification toolsets, compilers, debuggers and other developer tools for it. Updates to the language can be made directly in K. This technology has massive implications for smart contract programming language development, and formal verification efforts in the blockchain space. > We also cover his efforts to express the Ethereum virtual machine using the K framework, and to develop a new virtual machine technology, called IELE, specifically tailored to the blockchain space. Check out the episode to understand a game changing technology in the formal verification and smart contract safety space. > > Topics discussed in this episode: > - Grigore's background with NASA and work on formally verified correct software > - Motivations to develop K framework > - Basic principles behind the operation of K framework > - How K deals with undefined behavior / ambiguities in a language definition > - The intersection of K framework and smart contract technology > - Runtime Verification's collaboration with Cardano > - KEVM and IELE, smart contract virtual machines developed by Runtime Verification > - Broader implications of the K framework for the blockchain industry

>This development encodes category theory in Coq, with the primary aim being to allow representation and manipulation of categorical terms, as well realization of those terms in various target categories.

I listen to this (now very old) episode often to get inspired.

When John starts talking about compiling to categories, at around 14:40 to around 30:00, it gets REALLY interesting.

*😁😁 Hoping to bring this kind of discussion to the new Formal Methods community. 😁😁 * Here's the work he talked about: Compiling to categories by Conal Elliott

I need someone to get into the weeds on compiling programs to "axiomatized closed categories". What are the implications? What are the ramifications?

Here's the conclusion of the paper Wadler is referring to in this interview:

> Proposition as Types informs our view of the universality of certain programming languages. The Pioneer spaceship contains a plaque designed to communicate with aliens, if any should ever intercept it. They may find some parts of it easier to interpret than others. A radial diagram shows the distance of fourteen pulsars and the centre of the galaxy from Sol. Aliens are likely to determine that the length of each line is proportional to the distances to each body. Another diagram shows humans in front of a silhouette of Pioneer. If Star Trek gives an accurate conception of alien species, they may respond “They look just like us, except they lack pubic hair.” However, if the aliens’s perceptual system differs greatly from our own, they may be unable to decipher these squiggles. What would happen if we tried to communicate with aliens by transmitting a computer program? In the movie Independence Day, the heroes destroy the invading alien mother ship by infecting it with a computer virus. Close inspection of the transmitted program shows it contains curly braces—it is written in a dialect of C! It is unlikely that alien species would program in C, and unclear that aliens could decipher a program written in C if presented with one. What about lambda calculus? Propositions as Types tell us that lambda calculus is isomorphic to natural deduction. It seems difficult to conceive of alien beings that do not know the fundamentals of logic, and we might expect the problem of deciphering a program written in lambda calculus to be closer to the problem of understanding the radial diagram of pulsars than that of understanding the image of a man and a woman on the Pioneer plaque. We might be tempted to conclude that lambda calculus is universal, but first let’s ponder the suitability of the word ‘universal’. These days the multiple worlds interpretation of quantum physics is widely accepted. Scientists imagine that in different universes one might encounter different fundamental constants, such as the strength of gravity or the Planck constant. But easy as it may be to imagine a universe where gravity differs, it is difficult to conceive of a universe where fundamental rules of logic fail to apply. Natural deduction, and hence lambda calculus, should not only be known by aliens throughout our universe, but also throughout others. So we may conclude it would be a mistake to characterise lambda calculus as a universal language, because calling it universal would be too limiting.

sleet

A podcast with transcript which may help explain fp to laymen.

A great talk by one of the greats to get the ball rolling in this new community.

I was looking into the prospect of deploying an instance of Lemmy myself. Being an ULTRA nix fanboi (and a Docker-hater), I was immediately struck by how much the process still depends on (and, IMO, is being held hostage by) Docker containers.

Can we (or at least someone more capable and with more free time than I) help the Lemmy community by harnessing the power of nix and flakes to create declarative, reproducible Lemmy scratch-built instance deployment?

I suspect it would be exceptionally easy for some of you out there. If you are a flakes power-user, just think of how much this could help the community (and perhaps awaken a few people to the power of flakes).

ps. if this already exists, please point me in the right direction.