-
pmonson711
edited
1 month ago
|
link
| on:
If you could rewrite anything from scratch, what would it be?
My thought probably requires some time travel, so obviously a not realistic.
I would love to have a base cloud API that is supported by all major cloud providers. It would need to be something more than library with specific language binding, it would have to be defined (g?)RPC or REST API first, and have the tooling built around this. It would provide ways to deal with common compute, storage and network tasks in a way that you declare the dependencies between the base units so we don’t need to orchestrate outside the API for deployments that fit this base mold.
The API would need to support extension points that would allow the unique services and capabilities for the cloud provider. My hope for this is that the base API design will influence these extension’s and we would likely have a more consistent API even for the extensions.
The value I would hope this base cloud API would provide is removing, a ton of complexity from all the systems we now build to deal with any cloud system. I imagine if TerraForm/Ansible/Chef/Puppet/Salt didn’t have to implement these independently, they could focus on building out their own niche configuration philosophy more. Additionally, I think this base would simplify a self hosted cloud (on-prem, home or security lab). In the same way it may reduce vendor tie-in, but hopefully in a way that doesn’t hamper innovation at the cloud providers.
-
I get a “Video Unavailable: this video is private” message from that link.
I think the same content is being uploaded https://watch.ocaml.org/video-channels/ocaml2021/videos to watch after
-
-
It’s exciting to see the progress on Gleam! How do you plan to handle the heavily object-oriented nature of DOM code in general? Your examples use Reflect for assignment, but what if I want to call document.addEventListener or mutationObserver.takeRecords()? Or use the built-in Map type?
-
I expect we will have quite thick wrappers around DOM APIs that expose a limited subset of what is avalible that offers a stateful functional interface over the DOM’s OOP API. Similar libraries in PureScript and ReScript would be a good place to look for ideas.
The Map type can be wrapped fairly cleanly, it has quite a small and basic API.
-
In my experience, thick wrappers around platform APIs with huge surface areas like the DOM not effective in the long run unless they allow immediate escape hatches to the underlying platform. With strict segmentation or difficult interop, experts in the underlying APIs need to re-learn the facade abstractions you produce, and online learning resources need to be translated in the mind of the developer before they can be applied. Thick wrappers need maintenance to keep up with the platform, which is taxing on an emerging community. That isn’t to say wrappers are pointless, but they are a (in my opinion) very low local maximum unless there’s an easy escape hatch.
My case study here is React. React is a thick library over UI tree manipulation and state lifecycle. On the web, ReactDOM does great because users who want more can trivially access the underlying platform APIs: getting a DOM node and calling methods directly on it is a one line affair. But on mobile, React Native is extremely isolated from the platform. To call an unwrapped (or poorly wrapped) platform API requires writing platform-native code, serializing messages over a bridge between language runtimes etc. I rewrote Notion’s Android mobile app to remove React Native. I am not planning to rewrite Notion’s web app to remove React. Of course Gleam is not going to be so isolated from the platform — just using it as an extreme example.
Here’s how ReScript low-level interop looks directly against DOM objects:
// The type of document is just some random type 'a // that we won't bother to specify @val external document: 'a = "document" // call a method document["addEventListener"]("mouseup", _event => { Js.log("clicked!") }) // get a property let loc = document["location"] // set a property document["location"]["href"] = "rescript-lang.org"Does Gleam have a similar less-typed but more direct syntax for building the wrapper libraries?
It seems that Purescript prefers to write an “externs” header like file, and have the wrapper actually implemented in JS. Looking at the Purescript wrapper for MutationObserver object’s takeRecords method. Here’s the signature
foreign import takeRecords :: MutationObserver -> Effect (Array MutationRecord)And the implementation in the adjacent .js file:
exports.takeRecords = function (mo) { return function () { return mo.takeRecords(); }; };Between the two approaches, I much prefer ReScript.
-
-
One of the “newer” Browser API libraries I’ve worked with is https://erratique.ch/software/brr. It’s been a real pleasure to work with in js of oCaml, and the API seems to be very understandable. If you haven’t seen it yet it’s worth a look.
-
-
-
I think there’s an XY problem here. What’s the purpose of doing this? Is it because writing
<a href> </a>is too much overhead to write? Too much overhead to read? Is “links can only be one word” a technical limitation, or a design goal?-
-
Can you link to a resource that explains what you mean? I’m not familiar with 2D languages, but it sounds like you’re still using delimiters, they’re just white space instead?
-
I have no idea how the listed syntax is associated with a 2D language, but https://en.wikipedia.org/wiki/Befunge is an example of a 2 dimensional language.
-
-
-
-
https://github.com/zotonic/zotonic
Zotonic has been an incredible resource of inspiration over the years to me. Two things I particularly learned from it:
- The data model and caching approach is really easy to reason about.
- The “apps” (see the directory) show one of the best application component structures I’ve dealt with.
-
I felt this one. I haven’t been doing this, relatively, that long but it feels like we are eschewing formal documentation and planning for a more fly by the seat of our pants, get it right with enough iteration approach. I’ve talked to a few “technology savvy investors” in the past few years that have told me that software architects are an antipattern.
On the one hand the people against a more formal architecture approach might be right. If you break your features down to such manageable chunks that they can go from zero to hero in production in a sprint do we need need a full design process and documentation that will end up wrong or out of date before anyone has a chance to fix a bug?
I think the problem ends up being with the struggle of maintaining a cohesive architecture across all of these manageable l, hopefully vertical, slices of functionality. I’ve come into a few shops who have followed a low/no documentation route (“The user story is the documentation!” Said the project manager) and indeed they ship code fast but by the time I get there we get tasked with trying to build a unifying style or standard to move everything to because the original developers are gone/dead/committed to an asylum for their health and no one is willing to make changes to the legacy codebase with any confidence and ticket times are climbing.
So where is the middle ground? I would be happy to never have to create another 10+ page proposal, print it out and defend it in front of people who are smarter than me, and know it but there is something missing in modern software development and I think it’s some sort of process of getting our bad ideas out in the planning phase before writing code. Formal methods for sure fill this role but no one has the time outside of the “if my code fails someone dies” crowd.
I guess this is a long winded way of saying “I use formal planning to get my bad ideas out of my system before I create software that works but breaks in subtly or is just flat out wrong.
-
I think it’s a market thing. Subtly broken software that’s out now is better than well-designed software a year from now, from a customer adoption perspective….sadly.
-
I agree. Usually (hopefully) the lag isn’t that pronounced but it’s all how fast can we get a feature in front of users to drive adoption or validate our “product market fit” to investors. I’m glad where I’m at we have a formal architecture review, albeit abbreviated, for new features so we are trying to stradle that fine line between velocity and hopefully we’ll designed code. Sadly this just means the architect (me) gets a lot of extra work
-
-
Have you heard the good word of lightweight formal methods
(Less facetiously: the key thing that makes the middle ground possible finding notations that are simple enough to be palatable while also being machine checkable. I volunteer a lot with the Alloy team because I think it has potential to mainstream formal methods, even moreso than TLA+.)
-
-
The thing I really like about Alloy is that the whole BNF is like a page. So it’s not as big a time-investment to learn it over something like mcrl2 or TLA+.
Also, I think you’re the second person to mention mcrl2 in like a week, which is blowing my mind. Before this I’d only ever heard about it from @pmonson711.
-
I think I’ve finally warmed up to the idea of writing more about how and why I lean on mCrl2 as my main modelling tool.
Regarding Alloy and the time investment, I agree the syntax is much simpler. It did take me a huge mental investment to get comfortable with modelling anything that changes overtime. It’s a great tool for data structure/relations modelling but if you need to understand how things change with time, than TLA+’s
UNCHANGEDhandling feels like a necessity.-
-
-
I think I gave a less positive view of Alloy than I wanted in this comment. Alloy can certainly model time, but I always seem to end up ad-hoc defining the UNCHANGED much like the in the talk Alloy For TLA+ Users around the 30min mark.
-
-
-
-
The thing I really like about Alloy is that the whole BNF is like a page. So it’s not as big a time-investment to learn it over something like mcrl2 or TLA+.
I think that is a main selling point to me especially. I have a lot of interest in formal methods and modeling because i can see how damn useful it can/will be. Just carving out the time and the mental bandwidth to do it is a struggle. I am by no means good at any of the tools but I am putting a lot of effort to make the time investment worth it not just to me but the product as a whole. Currently I am trying to unravel my thoughts on how we apply/enforce a fairly granular security model in our system and its been a great thought exercise and Im fairly confident it will prove useful, or drive me insane.
-
-
-
-
-
While not in the same league, one may think of Kubernetes (also written in Go, BTW) as an alternative to the BEAM capable of orchestrating macro-scale processes (pods, services).
I have noticed this too. Can anyone from elixir confirm this ? I wanted to learn elixir just to avoid kubernetes but erlang concepts are just weird. There are people who tried to port more BEAM style solutions to go on github.
I am still not sure how different elixir is to deploying with lets say ansible + supervisord + python (with workers) on multiple servers, through an nginx proxy. Isn’t the real challenge of scaling database sharding, which is already solved by nosql ?
-
While not in the same league, one may think of Kubernetes (also written in Go, BTW) as an alternative to the BEAM capable of orchestrating macro-scale processes (pods, services).
I have noticed this too. Can anyone from elixir confirm this ? I wanted to learn elixir just to avoid kubernetes but erlang concepts are just weird. There are people who tried to port more BEAM style solutions to go on github.
Think of Erlang as its own OS and you’re not far off. It’s not weird, per se, it just doesn’t resemble the other OSes you’ve used before. Also, it’s not like k8s isn’t a little weird too :)
I am still not sure how different elixir is to deploying with lets say ansible + supervisord + python on multiple servers, through an nginx proxy. Isn’t the real challenge of scaling database sharding, which is already solved by nosql ?
Deploying Elixir is a non-issue. Throw it in a Docker container and do what you want with it, if you like. There is no single “real challenge of scaling”, but Elixir is there not to be the challenge.
-
So. I worked with a system that used to be ansible + uwsgi + python and I rebuilt it in elixir. It was a vm orchestrator (think bespoke ec2 for a special class of machine + customer). Maintaining the system with python was awful since it doesn’t really have a sane way to handle tracking state concurrently, especially when you are multidatacenter. Python forces you to think synchronously. When your objects go out of sync with reality you wind up in trouble (we had zombie vms all the time). Elixir by contrast makes you distrust any local data as soon as it’s obtained and guides you to smart strategies to handle conflict (crash the process and start over with a fresh pull of data).
However I had to leave when I was knocked down the org chart and the cto that was put between me and the ceo could not understand this.
-
When your objects go out of sync ?
How can this happen ? Can’t we use database/redis as the source of state ?
-
Yeah that’s the problem. The CTO wanted to treat the database as authoritative, when the source of truth was things IRL. It’s the object oriented mindset. And then I got blamed when stuff was not in sync, and the cto refused to create something that triggered a celery job to periodically poll my component to update the database.
And I couldn’t have my component write to the database, because it was in a different data center (not that that would have been a good idea, due to separation of concerns).
-
That sucks. I can see how elixir can make you think carefully about such state. That’s something I got out of a bit of clojure.
-
-
-
-
The authoritative information about the state of the vms lives at the edge, on the host machines. The authoritative information about customer intent lives in the database. So already there is something dangerous because information is not centralized. And it gets complicated. Suppose a customer does sudo shutdown from inside the vm instead of terminating from the dashboard (to be fair this was a huge problem for end users in the early ec2 days too). You have to think hard about reconciling these differences (and tolerating other corner cases, like netsplits or network disruptions, or orchestrator software redeploys, that might for reasons look like vm shutdown depending on how you are checking).
Elixir doesn’t do away with that need but it just surfaces these concerns early because it doesn’t try to hide them behind artificial abstractions like objects. As an elixir dev you get into the habit of distrusting (in the sense of is it stale?) any data that comes your way. Along with that mentality it provides a very convenient way of dealing with inconsistency or confusion: log it, crash your process, and have it restarted with a fresh pull of data, so you also don’t have to think about reconciling any data dependencies, because they will be populated in the way that you expect from the fresh pull.
-
-
-
José has an article about it, TLDR they work at different level’s
-
The section on partial failures is enlightening. Having faced something like it in python, I can totally see how it works … but itsn’t the crash and fail model similar to apache + php in that case ?
-
The key difference is the Erlang OTP model is often modelled in long running processes usually as gen_servers. Those processes are supervised and those processes are grouped such that failures are isolated. This structure makes it easy to reason about and isolate partial failures in your application.
You can certainly provide the same isolation in PHP, but it not part of the core PHP platform.
-
It is similar to many things:
- system supervisor restarting your application
- ASG restarting your VM
- CGI when retrying request
The main difference between BEAM platform and others, is that BEAM makes it layered and basis for most of its work. So restarting is very quick, that in many cases you shouldn’t even notice that. Additional thing there is that the failure is highly isolated - it causes only single process to fail - no other parts of your system are affected at all (for example failure in one HTTP request do not cause any troubles in other, concurrent, requests in the same system).
-
-
-
BEAM provides you with fault tolerance at the scale of a server rack, whilst K8S provides region failover. They do not operate at the same scale and this is by design. Now if you want, you can base an a big infrastructure on BEAM clusters, but you’ll be doing most of the hard work.
-
-
I found this very enlightening as to some of the difficulties of composing different specifications. I’ve often leaned on specification approaches that model processes and communication. I would imagine if you defined the blinkers as a independent processes (ala PlusCal) the composition would be closer to a developers intuition.
-
There’s a tricky subtlety here. PlusCal is a DSL that compiles to TLA+. If you look at the compiled TLA+, you’ll see that the different processes are represented by a global
pcstate that tracks the label of both. There’s no point where we have two specifications, we have just one specification with two subcomponents.The equivalent “composition” here would be putting two processes in separate files, compiling both to TLA+, and then writing a third spec that instantiates both files and composes
A!SpecandB!Spec.-
That makes perfect sense. I guess I’m trying to say PlusCal is designed to represent process and communication between them, and that composes well without the same difficulties described. It seems that is because they avoid the problems described of specification composing. The DSL could be used to compose a larger spec via careful concatenation. There isn’t really tooling to support it so not really any solution to the problem. But I find it interesting that re-framing the concept to an existing DSL may provide route to composition that matches a larger set of developers mental model.
-
-
-
I’ve used formal method tools at a few jobs, and I think something like this is incredibly important. Trying to introduce these concepts with “just traces” is not enough for a lot of people. They need to interact and see the effects of their choices on the system. That interaction, gives meaning and trust to them for these processes and tools.
One of the reasons my go-to tool for understanding and specifying these days is mcrl2 simply because it makes interaction with the spec so easy with it’s simulation tools. But I often find the difficulty of getting to traces troubling.
-
One of the reasons my go-to tool for understanding and specifying these days is mcrl2 simply because it makes interaction with the spec so easy with it’s simulation tools. But I often find the difficulty of getting to traces troubling.
I’ve tried to learn mcrl2 a few times and keep bouncing off. Someone needs to write a good showboating example for it!
-
-
It appears to be removed from the netgate site now. Here’s a web archive link:
-
I think there is a nice simple truth in “Complexity has to live somewhere” that is creates great conversations when designing any system.
I’ve been reading through everything I can find on https://en.wikipedia.org/wiki/Problem_frames_approach which is the best system I’ve seen that helps make that complexity tangible to a group. The key aspect of the PF approach the helps show the essential complexity is its process of describing the real work effects and constraints, by limiting your “machine” gather info and triggering effects to a real world entity it feels like I actually can separate the essential complexity from the accidental complexity.
I am curious if anyone else has a process / thought tool to help show where the complexity it.
-
Enjoyed the article. I’ve been slowing introducing formal methods as a design simulation and engineering thought tool. Basically, matching what the article discusses as debuggable design. One thing that I’ve found is hard for most software engineers is that they structure their specs like a system, not like a set of purer logic.
To help get of over that boundary I’ve spent a lot of time with mCrl2 which allows the spec to look much closer to a system. But, I’m curious if anyone has advice on limitations of that toolset in comparison with TLA+ or Alloy?
Perhaps, I need to write a mCrl2 version of articles example to show how it would look different…
-
-
For those that are interested in formal methods and haven’t seen mCrl2 before, I’m including my notes on what I belive makes it unique. I’ll include some links to parts of it’s toolset which aren’t covered specifically in it’s tutorials which fill roles you may be used to like generating counter examples and checking invariants.
- It excels at modeling how a system communicates. It models actions (which I think of as observable elements of a process) and state as 2 separate concerns. This has proven a valuable separation when modeling separate components/services of a larger system.
- It has a tremendous amount of tooling to describe how two specs are different. This really helps understand how a spec can change over time, and if those changes require updates to the different components. It also can help in finding simpler models in theory but I’m less sure how that process would be realized.
- The simulation helps both writers and readers of the specifications gain confidence it matches their expectations. It’s like having a usable REPL to each of your specs. The simulation also comes both with state visualization GUI tools which helps less technical folks remain engaged in the spec.
- It’s really helpful to be able to start with an FSM and convert that back to a process definition. My mind was blown when I realized the power of it’s different formats. Don’t skip on understanding the LTS Formats what what it means to check them for similarities. It might be a different way to specify things, but I’ve found it to be a great way to explore different solution approaches.
- The way mCrl2 deals with time, and asserting properties over time is really hard to grasp. Somehow I can’t internalize the meaning of the mu-calculus it uses. It seems like the most powerful tool it has, but I can’t find a way to describe it to others; so I’m sure I don’t understand it yet.
- It took me too long to find the tooling for asserting invariants. But it seems like a nice enough setup to it. I imagine this is the “easy-mode” where most examples use the mu-calculus I’m still trying to understand enough to use.
- Most tools can generate counter examples with a flag. Usually
-c, but you often have to review it as a graph or then check it for other things like deadlocks to get a clear trace, like you get directly out of TLA+.
Overall, I think it sits in an interesting place for formal methods. It’s less abstract (and less like pure logic) which makes harder to write directly off of requirements. Having said that I think the tutorials show lots of examples where going from a set of requirement can be specified and tested. When I compare it with TLA+, Alloy or VDM it’s exists somewhere between the TLA+ and VDM, perhaps closer to B or Z; but I have no experience with those. Finally, the simulation side of it has been the mostly incredibly valuable tool for sharing the specs. It also helps validation while writing which I now miss when utilizing other methods.
I would love to hear anyone else’s experience with either mCrl2 or how they share spec’s with teams and get the teams to gain confidence in them.
-
-
-
I’ve found yEd to be a great fit for network diagrams. The combination of features really works well, with a visual tool and a the automatic layout options.
-
-
Surprised they didnt cover observer, the trace tool and the crashdump viewer.
-
Observer is such a great tool, especiallyfor those getting used to OTP process, and supervision.
-
-
As a Elixir developer who has dabbled with Go in the past, I found this post hits really close to home. One topic I do think needs further writing on is ‘why’ & ‘when’ to choose between something like Go and Elixir. Personally, I don’t see a large overlap of where I would use these too languages, but that is likely because for most service/web/network development I would reach for Elixir; and that covers the vast majority of what I write today.
-
Work
- Working on a top to bottom monitoring plan for upcoming projects and how that will work with our hybrid cloud and DevOps tool sets.
- Create hiring plan for upcoming projects
- Delving deeper into Elixir and Phoenix on my usual CMS setup to learn a language and platform
- Testing out dynamic Routers for Phoenix to support my “plugin” system for the CMS
-
The correlation of EAV schema’s and JSON columns is a great point, and I think the post does a great job of simplifing the problem to show exactly how similar the two approaches can be.
But I can’t help but think EAV presents many different values then JSON as your code base changes. For example if you look at the Zotonic it’s data model is an EAV schema, based on something like RDF triples. It stores the binary of the code terms in a column… which I’m not a fan of at all. But it does have a very nice system of pivot tables which point back to the “Entity” resource table. This seem much more natural to me than either he JSON or embeded binary.
-
This is a classic article from Fred, if your looking for more info about handling issues like this in the erlang world see his ebook http://www.erlang-in-anger.com/
-
I love the presentation & content. Any chance you can share some the the source or do a write up on how you built it?
I think (hope) the techniques of formal methods can be used to better describe systems of systems. Having a specification of how a set of services interact has long been a dream of mine. The types of properties I would love to prove are:
One aspect of this that think needs better tooling and exposure is creating more meaningful simulations. I imagine other approaches might work but my personal experience with using formal methods in a organizations end with “that’s magic I don’t trust it”, “I don’t understand the presentation of this” or “I think the journey is more important that the outcome”. The few break through moments I’ve had are with simulations[1]. I think that this simulation approach allows a wider audience and meaning to any investment in a specification.
[1] https://runway.systems/ or https://www.mcrl2.org/web/user_manual/index.html
Who’s got two thumbs and just received his copy of Modeling and Analysis of Communicating Systems?
this guy
Probabilistic model checking can also help a bit with this.
That’s an interesting idea. I’ve purely looked at it from an ordering of events or actions. If you have any recommended toolsets or articles about that, I would love to try them out.
PRISM introduced probabilistic model checking. There’s a lot of literature, tutorials and case studies associated to it: https://www.prismmodelchecker.org/