HNHacker News
TopNewBestAskShowJobs

kreneskyp

149 karma · joined July 17, 2009

Lead Software Engineer for the OSU Open Source Lab
submissionscomments
kreneskyp··on Developing provably correct Rust code with Verus
I'm working on a ISO-29148 aligned spec standard with formal modelling baked in. It's meant to sit above the code with types, contracts, proofs and other objects that lower mechanically into code and/or are deterministically verified.

I'm targeting Rust primarily but my goal is that any language could sit under it via an integration layer.

https://github.com/agent-ix/quoin

The first public version of the formal specification standard isn't available yet. Pushing hard to get it out soon! But Quoin ships with an earlier version of the spec standard. It features derived property tests, which was the POC for fully adopting a formal-spec-to-derived-formal-verification ecosystem.

kreneskyp··on Towards Self-Driving Codebases
My answer to this is adding an engineering assurance module to my specification and verification toolkit. Every project has a different definition of success and quality. My goal is to provide a consistent way to define, analyze, and report quality metrics tailored to each project.

https://github.com/agent-ix/engineering-assurance https://github.com/agent-ix/quoin

kreneskyp··on Vibe coding and agentic engineering are getting closer than I'd like
> If you're trying to learn something new like an algorithm, protocol, or API write that shit by hand. You learn by doing, and when you know how the thing works and have that mental context, you will always be faster than an AI. Also, when did we stop liking to learn?

I vibe engineer to learn. I am currently doing this with a project to build a Vector DB extension in postgres. Several aspects of this project are very new to me. I don't write any of the code. I have never written a single line of Rust. I do, however, spend a significant amount of time discussing architecture and design with the agents.

I started with well known algorithms (HNSW, IVF, DiskANN, TurboQuant, RabitQ, PQFastScan) and have since moved on to a novel implementation based on fairly recent research papers.

My primary goal is to learn. That is a success and ongoing. A stretch goal is to contribute novel ideas back to the community, which may be useful even if what I build isn't ever production ready.

kreneskyp··on Blueborne – A new attack vector endangering major operating systems
For android: https://play.google.com/store/apps/details?id=com.armis.blue...
kreneskyp··on SCOTUS Rejects Guilty Until Proven Innocent – Can't Keep Money from the Innocent
Can you expand on why civil forfeiture based on suspected criminality shouldn't require criminal conviction? Forcibily taking money from someone for a civil reason (e.g. child support) is obviously different from taking money because you suspect a criminal offense.
kreneskyp··on Reddit Gearing Up to Ban or Quarantine the Alt Right Subreddit
I don't think you're familiar with /r/the_Donald's rules. The number one rule is no dissenting. Not even polite discussion is allowed. They've already entombed themselves.
kreneskyp··on Reddit Gearing Up to Ban or Quarantine the Alt Right Subreddit
It's not discrimination to enforce site wide rules against harassment, racism, and brigading (coordinated upvoting). Just because only a few communities are breaking the rules doesn't make it discrimination. Racists and bigots aren't a protected class.
kreneskyp··on FBI Reopens Clinton E-Mail Probe Less Than Two Weeks Before Vote
You left out Petraeus who did worse and still only received probation.

The reality is that most cases of mishandling classified information result in little more than a stern talking to from your manager, re-training, and a blemish in your file.

kreneskyp··on FBI Reopens Clinton E-Mail Probe Less Than Two Weeks Before Vote
Back that assertion up with polling data. The polls I've seen show the opposite.

edit: referring to the claim that Clinton voters aren't voting for clinton

kreneskyp··on House panel looking into Reddit post about Clinton's email server
They were subpoenaed by Congress, but not until March 4, 2015. The initial request for emails was made by the State Department.

Edit: small mistake. The initial request did come from Congress and went through the State Department. It was not a subpoena though, that came later.

Edit 2: Since it was clear to some, the reddit post was dated July 24th, 2014. That's 7 months, prior to the first subpoena.

kreneskyp··on FBI Releases Documents in Hillary Clinton E-Mail Investigation
You're not guilty just because a cop says so. You have a right to a trial for every speeding ticket. Most people just waive that right.
kreneskyp··on Catching a Flight? Budget Hours, Not Minutes, for Security
Abolishing the TSA doesn't mean ending airport security. It would mean replacing it with privatized security. The TSA is universally hated so it wouldn't be that hard to find enough Democrats to go along with it.
kreneskyp··on TSA can now force you to go through body scanners [pdf]
They said they don't generate or store images period, which is at best misleading. It might not generate or store a commonly used image format, but it's still an imaging machine. The machine generates images or it's pure security theater. Either way they are attempting to deceive people and they shouldn't be trusted. (doubly so since previous claims that they don't store images is a proven lie)
kreneskyp··on As of 9.5, Postgres JSONB data can be modified
This is only partially correct. These new features reduce the amount of data that must be transmitted to/from the postgres server and how much json must be parsed, but the full row is still written to the WAL (write ahead log). This is true even for partial updates to JSONB columns and even when only updating other non-JSONB columns in the row.

When you do need to update JSONB columns this is a big improvement. You still should consider the size of your JSONB columns and the number & frequency of updates to those rows.

kreneskyp··on Making Connections to Facebook More Secure
Yes. If someone captures identifiable information then a user can be identified. This can be minimized by using SSL to connect to services. A service may share data so you should also use only a single service within a Tor session. That includes closing tabs to prevent ajax requests.

A new session can be created by restarting Tor or from the tor indicator if within TAILS.

kreneskyp··on Ubuntu TV unveiled
There is zero chance of content without DRM and probably requires locked hardware too. Boxee and Android (cant rent movies on rooted devices) had those requirements for content deals, Ubuntu won't be any different.
kreneskyp··on Time to end the war on drugs
The idea of "drug tourists" is absurd. The worst of the illicit drug addicts can barely take care of themselves. They choose drugs over food and showers. They can't hold jobs and resort to crime to feed their habits. Access to drugs isn't their problem else they wouldn't have become addicts in the first place. They aren't going to spend their money to travel to Portugal even if they can afford it.
kreneskyp··on Why developers should be force-fed state machines
The problem is that many apps are looking at the wrong states when they design their machine.

For instance I worked on an app someone had build in which states were based on a multi-page html form. When I added an android app allowing offline data collection, I then had to hack around the state machine. We couldn't just create a instance of the object with the final data, we had to write code that replicated the submissions of the html form.

kreneskyp··on Chromebook Pre-Orders Now Available to All
Google never said when the emails would go out.
kreneskyp··on Copenhagen Suborbitals open-source private spacerocket will launch in an hour
For those of us without silverlight: mms://itv02.digizuite.dk/tv2b

VLC can play it but the server is getting hammered right now. Received 503 the first few tries but then it loaded.

kreneskyp··on Photo tour of Facebook’s new datacenter
Hah. You got me there.
kreneskyp··on Photo tour of Facebook’s new datacenter
There were various things we weren't allowed to take pictures of but mostly they were very open. You can't even get to the bathroom without a keycard. I don't think they have a reason to be paranoid.
kreneskyp··on The Google I/O freebie I'm hoping for: Nothing
I didn't see a reason why they sent them early last year anyways.
kreneskyp··on The Google I/O freebie I'm hoping for: Nothing
Several co-workers and myself are road tripping it from Oregon and splitting hotel rooms. We're all self funding to go. I can't speak for the others but I'm interested in the sessions, though without potential freebies it would have been a much harder decision.
kreneskyp··on Introducing Supercell: test infrastructure for any open source project
It differs in that this isn't just Hudson or some other testing software. We're providing a self service cloud that open source projects can use in lieu of Amazon, Linode or other paid providers.

Eventually windows support will be added. KVM/Xen supports it, so Ganeti does also. Where we're lacking is code to deploy a windows image on demand using Ganeti. We've started talking about how to implement it, but linux and unix based environments remain our primary target.

kreneskyp··on Introducing Supercell: test infrastructure for any open source project
Ganeti. It sits a layer above KVM or Xen. The main difference from KVM proper is that it allows management of multiple KVM servers and storage nodes as a single cluster. You get failover, easy migration between nodes, balancing, etc.

With Ganeti Web Manager we're building towards software that will let you manage your own private or public cloud service.

kreneskyp··on Stuxnet is embarrassing, not amazing
according to leaked cables some middle eastern countries actually encouraged us to bomb Iran. Otherwise I agree that a non-military solution is at least initially appealing.

  I fear whoever unleashed this has opened a pandora's box of destructive malware.  We've already seen things like China hacking major corporations and manipulating it's currency.  It's not hard to picture a future where malware is used to hurt the competition's production, at either a corporate or state level.
kreneskyp··on Car theft by relaying signals from wireless keys
RFID range is between 3-20 feet. Average human arm length is less than 3 feet. The limiting factor here is not RFID range.
kreneskyp··on Car theft by relaying signals from wireless keys
Just because it's "active" doesn't mean the FOB needs a battery for the RFID to work. The car could periodically check for the key.

If your RFID required a battery, and required that it constantly be on, then the battery would need to be replaced often. Couple this with your car potentially shutting off in the middle of the highway and you've got a very unsafe car.

I know for certain that VW keys do not need the battery for the RFID to work. The battery is only used for remote lock/unlock. Perhaps other cars are different, but I'd consider that a design flaw.

edit: forgot to mention that my VW does not even have physical locks except for the glovebox. A dead rfid battery, if it had one, would mean i was stranded. I'm actually not sure what happens if my car battery dies while the car is locked.

kreneskyp··on Car theft by relaying signals from wireless keys
The key doesn't have a battery. It's usually RFID.
Page 1 of 3Next →