I tried it not long ago - it's really cool just a tad sad that the rust eco-system didn't allow verus to be more streamlined in the tool and requires these little shenanigans with a different build of it - it felt a bit clunky to swap cargo for the verus one ; but the tool is definitely needed right now

So far out of what I've looked at, Kani blends into the Rust language best. Verified code snippets look a lot like unit tests.

  #[kani::proof]
  fn check_my_property() {
     // Create a nondeterministic input
     let input: u8 = kani::any();

     // Call the function under verification
     let output = function_under_test(input);

     // Check that it meets the specification
     assert!(meets_specification(input, output));
  }

It looks like fuzzing, but it's proving no-panic for all possible values symbolically. If only it handled loops better :-/

Verus wraps everything in its macro that makes rust-analyzer etc unhappy.

Do you have any reference to the Rust community “not allowing” something? This seems more like a case of a relatively niche tool doing what it needed to do to work, but not (yet) some broader effort to upstream or integrate this into cargo or rustup. I couldn’t find any RFCs or anything, for instance.

I didn’t read OP as saying “the community won’t allow” but more “the tooling doesn’t allow” for what they want to do.

"You’d think telemetry is screen recording your every move" - that's literally what tracing and telemetry is about.

"Sure, you can spend the weeks to months of expensive and time consuming work it takes to get a fuzzy, half accurate and biased picture of what your users workflows look like through user interviews and surveys. Or you can look at the analytics, which tell you everything you need to know immediately, always up to date, with perfect precision." -> your analytics will never show what you didn't measure - it will only show what you already worked on - at best, it's some kind of validator mechanism - not a driver for feature exploration.

This kind of monitoring need to go through the documented data exposure - and it's a sufficient argument for a company to stop using github immediately if they take security seriously.

But I'd add that if you take security seriously you are not on Github anyway.

Fun is not always about finding up the exact look or design of something - you might be having it for your own particular reason - and by the time a website has to present it might have shifted already. That's why these land and why we might be confused about the process

I kind of agree with the comment here that a lot of stuff happening around comes out from an idea without proof that the project has a meaningful result. A compacting memory bench is not something difficult to put off but I'm also having difficulties understanding what would be the outcome on a running system

I have been using the memory while building it. I have a central server and all my workspaces are connected to it via the MCP server. This changed everything for me. But that's me. Now I don't have to repeat things, the agent knows my preferences, can connect different projects I am working on without me asking and it knows my infra so can plan the test deployments and stuff on its own. That is somewhat I was aiming for.

Same hack here ; I have no DSN running by default - much more handy than having to set up nginx as it has no opinion on the targeted infrastructure. And the bonus point is that you can see every sneaky request that happens when you browse ; so another side-project connected to this is to make an inventory and policy filter

Yes sir! The query log is at GET /querylog (or on the dashboard) shows every request with domain, type, path (forwarded/recursive/cached/blocked) and latency

1kloc is a bit abstract ; it seems you are in a great position to give a true bundled weight ; preact is about 3kb which is my fav for years - good job for the effort and results !

The library is actually ~1400 lines of code, and 51KB in size. Not very slim by JS framework standards, so focusing on that for the headline feels misleading.

9kb (minifier+brotli)

We could remove 3kb by removing the router but that's not gonna happen. You're more than welcome to minify+brotli it yourself if you use vertex.js in production.

"What I learned" - where ? couldn't be more bait-click.

I'm very surprised it's *that* short - handling one in rust i'm surprised by the very low amount of code to get that up. Thanks or sharing that was a first time reading some Zig for me !

what you’re experiencing is more or less why I am building some stuff in Zig instead of Rust

Looking at the code, I'm not really sure what part of this would be more verbose in Rust. This kernel does close to nothing, not even page table setup.

Granted, the code writing to the VGA buffer will need to be in `unsafe` blocks, but yeah.

it doesn't have a bootloader.

What's the point writing another kernel in C ???

Considering that we are talking about experimental toys which have lower odds of seeing production than of you winning a national lottery jackpot, the point of writing it in C would be the same as the point of writing it in anything else - IOW, the kernel is the objective, not the language used to write it.

.

If you read yourself you'll realize your answer i highly toxic, quiet honestly completely irrelevant, discouraging other people from doing what they like. I would get rid of people with your attitude, you are the kind of problem I don't want to have to deal with and more than that, I don't want to have juniors have to deal with you. Please realize that you had your chance and you played it. Nobody ow you an explanation if you can't even get basics up.

What in the sweet chili dipping sauce did I walk into?

drnick1 says why "Zig" not C? [I took the quotation marks as dismissive of Zig, but I could be misreading that]

6r17 says why do it in C?

lelanthran says the language is mostly irrelevant, it's a fun experiment.

6r17 blows off the handle and starts calling people toxic and being really unpleasant.

Nothing in this comment chain seems to justify even 1/10th of the vitriol espoused.

"Considering that we are talking about experimental toys which have lower odds of seeing production than of you winning a national lottery jackpot"

If you think that quote above is at all proportionate or justifies your toxicity, we have nothing else to discuss.

Yeah, but even if I'm doing something for fun I do want to be a bit unique with it. Anyone who's interested enough in osdev to build something for baremetal has at least attempted a unix-like kernel in C

I don't know - i'm 33 ~ now - recently with AI learning is much easier - don't get me wrong I definitely won't say that the brain does not slow down - but I'd definitely argue that we have advantages over kids - be it discipline, knowing how to learn ; and stuff like that - for example let's take coq which is I suppose one of the hardest thing we can learn - you can decompose it in ways myself as a kid or as a 20yo wouldn't even be able to. What I mean is that there is a lot of complexities or stuff i would get stuck upon that I just fly over today and know I'm alright - much better ability to focus in a sense

I learned coq as a teenager because the name was funny and one defined everything in terms of the `succ` function.

Never underestimate our motivation.

Continuing to do things only because they’re funny as an adult is one of life’s little treats!

Unfortunately, they changed the name to Rocq.

...as long as they also changed the defining function to `hard`, we're still good.

I wonder if everyone who said it was a lot easier for them to learn when they were younger aren’t factoring in their increased responsibilities as an adult.

I know when I’m actually able to sit quietly to study something, I’m able to pick it up fairly quickly. (One thing going for me is I’m much better able to sit still as an adult than a kid, ha.) But yeah, having to juggle work responsibilities for 8-9 hours a day and then having to also manage a bunch of things I didn’t have to think as hard about when I was younger (bills, cleaning, pets), I definitely just don’t have as much time to dedicate towards focused studying like that.