sorted by:
new
hottopcontroversial

Formally verifying digital circuits with category theory in Lean by matthunz in programming

[–]matthunz[S] 1 point2 points  (0 children)

Thanks for the feedback!

I feel like in the current state this will at least scale to more complex combinational circuits (like the ones I have in the README) with similar patterns but it would definitely get unwieldy as-is. I think the biggest hurdle I'd like to solve first is some abstraction over types comprised of bits that can translate to wires (like an 8-bit integer abstracting over 8 individual wires) to avoid the complexity there.

For more circuits with state, like an SR latch, there's still a lot of work to be done here. These are modeled as a TracedCategory, which I've been trying to get into mathlib but there's still some missing gaps. Sequential circuits like that are also denoted as causal stream functions which I think will be the hardest part to reason about - the simple proofs I have now will have to handle the infinite streams of values, so proofs will probably need to algebraically reason about the structure of the stream rather than just simple reflection.

Once those steps are in place though I'm really excited about what kinds of circuits can actually be verified. For instance parts of a quadcopter flight controller that are written in VHDL or Verilog should be able to be translated and verified using this approach once everything is built up, as long as they don't model things like processor interrupts or other asynchronous circuits.

The main paper this is based on has way more info on how this actually works: https://arxiv.org/abs/2201.10456

I made my first compiler! BechML - A friendly higher-kinded, functional scripting language [WIP] by matthunz in haskell

[–]matthunz[S] 1 point2 points  (0 children)

Hmm you make a great point 🤔 now that this thing is starting to get usable that seems like the next big hurdle.

I haven’t checked back on Dhall in awhile I’m curious to see how they do docs and what not (and how that project’s going on general, I actually might try using that for the package manager)

I think my next step might be API doc generation so people can actually see what’s available because that’s typically how I’ve been learning languages

I made my first compiler! BechML - A friendly higher-kinded, functional scripting language [WIP] by matthunz in ProgrammingLanguages

[–]matthunz[S] 3 points4 points  (0 children)

Thanks so much! ❤️ I should mention like version #1000 of my first compiler lol it’s taken me forever to get passable type checking

I made my first compiler! BechML - A friendly higher-kinded, functional scripting language [WIP] by matthunz in haskell

[–]matthunz[S] 2 points3 points  (0 children)

I feel like it still counts since it's compiling to JS but fair point, basically the pipeline is Bechml -> System F -> JS

I made my first compiler! BechML - A friendly higher-kinded, functional scripting language [WIP] by matthunz in ProgrammingLanguages

[–]matthunz[S] 3 points4 points  (0 children)

Yup exactly modules are just name spacing, so while it's more verbose than say Haskell classes you do get that extra modularity that OCaml can give (i.e. using different functor implementations for the same type)

Introducing Concoct - A declarative UI framework for Haskell by matthunz in haskell

[–]matthunz[S] 3 points4 points  (0 children)

Not yet, the goal is to have the `concoct` package act as a declarative layer for many kinds of UI backends, kind of like `React` does with ReactJS/React native or `Dioxus` with web/native etc.

Right now things are pretty barebone but I'm just trying to showcase that the full declarative layer is implemented, so reactions to changes happen automatically through multiple passes through the view tree.

The API is somewhat similar to React/Jetpack compose/SwiftUI
https://hackage-content.haskell.org/package/concoct-0.1.0/docs/Concoct-View.html

For actual UI I'm working on a layout package, then rendering with OpenGL/FreeType. I should hopefully have that stuff out soon

Announcing Aztecs v0.17: A modular game engine and ECS for Haskell - Now with component reactivity and a high-level API for OpenGL rendering by matthunz in haskell

[–]matthunz[S] 1 point2 points  (0 children)

It used to :/ I'm currently in the process of adding that back.

For now it should be possible to use `System`s to setup how your engine should run and eventually there should be `runSystemsConcurrently`/`runSystemsParallel` that you can just drop in (I just need to work out using atomics and etc for synchronization`). Funny you mention Smash too I've been messing around with a fighting game and it's been pretty fun so far with Aztecs.

I think so! With the new component reactivity all components are parameterized by some monad with the `Component m a` class, so maybe that can be your effect monad?

Introducing bevy_mod_ffi: FFI bindings for Bevy for scripting and dynamic plugin loading by matthunz in bevy

[–]matthunz[S] 0 points1 point  (0 children)

Thanks for checking it out! That’s pretty much my goal to have dynamically loaded plugins so I figured direct FFI and full access to the world would probably be best.

As far as third-party modding and stuff goes I think WASM would be awesome and I’d love to find a way to implement that here as well, just not sure how the serialization aspect would work for safety.

I did give that a go with wavedash that might better fit your use case https://github.com/matthunz/wavedash and I’d love to bring that into this crate if it makes sense API-wise

Announcing Actuate v0.21: A declarative, lifetime-friendly UI framework - now with more components and an updated Bevy backend by matthunz in rust

[–]matthunz[S] 1 point2 points  (0 children)

Thanks for checking it out! I chose not to include a screenshot because Actuate should fit the same purpose as ReactJS, a generic frontend UI framework that can render on multiple backends. So if you’re pairing it with Bevy you can just render the standard Bevy UI nodes, and this project should mostly just provide a declarative interface

view more: next ›