Thursday, December 4, 2025

Killing Voicemail with Twilio: A Simple Setup for People Who Hate Voicemail

I hate voicemail. My inbox was mostly full of robocalls, accidental pocket dials, and 'call me back' messages that would have been far clearer in writing. Eventually, I decided that voicemail had to go.

The solution turned out to be wonderfully simple: instead of letting my carrier send unanswered calls to a traditional voicemail box, I now forward them to a Twilio number that plays a short, polite message and immediately hangs up.

Step 1: Get a Twilio Number

After creating a Twilio account, I rented a local phone number. This costs me $1.15 per month.

Step 2: Create a TwiML Bin

Twilio uses TwiML (Twilio Markup Language) to define call behaviour. In the Twilio Console, I created a new TwiML Bin containing my greeting logic.

Here is a sample XML:

<?xml version="1.0" encoding="UTF-8"?>
<Response>
  <Say voice="male">
    Hello. I do not use voicemail. Please send me a text or email instead. Goodbye.
  </Say>
  <Hangup/>
</Response>

This answers the call, speaks the message, and hangs up immediately. If you prefer a recorded audio file, you can replace <Say> with <Play> and point it to a publicly accessible MP3 file.

Step 3: Connect the TwiML to the Number

In Twilio's number settings, I set the Voice configuration to use my new TwiML Bin. Calling the Twilio number now plays the message and disconnects properly.

Step 4: Forward Unanswered Calls to Twilio

Here is the key part: telling my mobile network to forward all conditional calls (busy, no-answer, unreachable) to this Twilio number instead of voicemail.

On T-Mobile US, that is done with a single GSM code:

**004*<TwilioNumber>*11#

Dial it on your phone, press call, and you will receive a confirmation. This ensures any call that would have gone to voicemail is redirected to Twilio instead.

To remove forwarding later, dial:

##004#

What It Costs

Twilio charges:

  • About $1-$1.50 per month for the virtual phone number.
  • About $0.008-$0.009 per minute for incoming calls.

Because my greeting is under 10 seconds, each forwarded call costs only a fraction of a cent. Even ten missed calls a month add up to only a few pennies.

Future Possibilities

The setup leaves plenty of room for adding smarter call handling later on.. In the future, you can add:

  • Different greetings or handling for different callers.
  • Automatic SMS replies explaining why voicemail is disabled.
  • Integration with email, messaging apps, or your calendar.
  • Logging or analytics to see who tried calling, without needing voicemail.

And That's It - Voicemail Is Gone

Now, whenever I ignore or miss a call, the caller is forwarded to my Twilio line, hears:

"I do not use voicemail. Please send me a text or email instead."

...and the call ends. There is no mechanism for leaving a message. My voicemail inbox is gone, notifications are gone, and life is significantly quieter.

Friday, November 28, 2025

Essence and Accidents of AI-Generated Proofs

There is an ongoing, sometimes heated, argument between people embracing AI "vibe coding" as a great new technology liberating us from mundane tasks and allowing us to focus on high-level problems, vs people considering it is "stupid autocomplete" which produces "AI slop" while dumbing down writers who routinely rely on it, in the process.

We will frame this discussion around AI-assisted proof synthesis (e.g., for the Lean proof assistant). While proof and code synthesis are conceptually similar (by the Curry-Howard correspondence), the former is more illustrative in an academic context, as it brings questions of originality, attribution, and credit assignment into sharper focus. Additionally, there are a couple of important differences pertinent to using AI:

  • Correctness criteria. Once the theorem is formulated, the proof assistant can check the candidate proof and determine whether the given theorem statement is indeed proven.
  • Proof irrelevance. Any two proofs of the same proposition are considered indistinguishable and equally valid.

These differences address concerns about the correctness of generated proof (which can be checked) and eliminate the need for human review, thereby invalidating the "AI slop" concern (style or verbosity does not matter, as the proof term is intended for the checker, not for humans).

🧠 Informal Problem
        │ 👤 Human — formalisation
        ▼
📄 Lean Specification
        │ 🤖 AI — script generation
        ▼
📝 Proof Script
        │ LΞ⋀N — elaboration + checking
        ▼
✔️ Verified Proof Term

This leaves us with more fundamental questions: 1) Can the AI-generated proofs be considered genuinely innovative or just a rehashing of existing prior work? 2) How much of the result could be attributed to the individual vs the machine?

The first question is a topic of ongoing debate about AI, which goes beyond proof or code synthesis applications and is outside the scope of this essay.

To answer the second one, we first informally divide proofs into two broad categories. The first type of proof is primarily mundane and mechanical, for example, as is common in proofs in program verification, which usually involve structural induction, case splits, term unfolding, and normalisation, etc. Such proof generation could be viewed as automation, similar to SAT solving, using decidable theories such as Presburger arithmetic or using tactics such as the "Sledgehammer" in Isabelle/HOL.

The second type is more intricate proofs in which the solution is non-trivial and requires making deep observations about the nature of the problem, linking it to external theories, identifying relevant invariants, and introducing and proving new conjectures.

Intuitively, the first kind involves no innovation or creativity and requires no credit for intellectual contribution, while the second calls for assigning intellectual credit.

These two categories may correspond to the "accidental" and "essential" difficulties described in [1]. In the context of mechanised proofs, essential difficulties are inherent to the nature of the problem. In contrast, accidental difficulties stem from the mechanics of formalisation, such as proof automation, combinatorial explosion, representational bottlenecks, and limitations of the proof assistant. But is there a precise boundary between these two?

Accidental Complexity Essential Complexity
structural induction finding the right abstraction
case splits identifying key invariants
term unfolding / reduction introducing new definitions or concepts
normalisation / rewriting linking to external theories
proof repair / refactoring formulating auxiliary lemmas
heuristic lemma search discovering new conjectures
managing combinatorial explosion reframing the problem conceptually

Let us reflect on the pre-modern-AI era, on computer algebra systems like Maple or Mathematica, which can symbolically solve some differential equations. Mathematicians typically do not list Maple/Mathematica as coauthors. Back then, one might say that the problems such a system could solve are merely accidental difficulties. Conversely, if it could not be solved by it, the difficulty may be either essential or accidental.

Unfortunately, with modern AI, we can no longer use such a simple distinction. It is claimed, albeit still a matter of debate, that modern AI may exhibit emergent properties that go beyond what it was trained on. This leaves the possibility of producing truly innovative results and thus solving problems of essential difficulty.

Unsatisfactorily, this leaves the line between the proofs of accidental and essential difficulty not firmly fixed. It remains a judgment call. Moreover, historically, such a line has shifted: many mathematical proofs of problems that were regarded as essential in the 19th century are now treated as accidental, as the development of new methods turned once-insightful arguments into routine applications.

As of the time of this writing (November 2025), the type of proofs which AI could reliably generate falls into the first category: mundane and mechanical (accidental complexity). So if you are using AI to grind out these proofs, it would be safe to consider it just an automation aid that could be used without reservation. As the state of the art in AI models evolves and they can tackle the essential complexity in proofs, we may need to start crediting them for their contributions.

References:

[1] Brooks, "No Silver Bullet Essence and Accidents of Software Engineering," in Computer, vol. 20, no. 4, pp. 10–19, April 1987, doi: 10.1109/MC.1987.1663532. https://www.cs.unc.edu/techreports/86-020.pdf

Wednesday, March 26, 2025

Evolution email setup for Tufts.edu

If anyone is trying to set up the Evolution email client to access a Tufts University (tufts.edu) email account, I hope a Google search leads you here! After spending some time on this, I want to document the working steps for the public record.

  1. When adding an account start with your official email address John.Smith@tufts.edu
  2. Untick "Look up mail server details based on entered e-mail address". (the auto-discovery does not work and takes forever.)
  3. Use Microsoft365 account type (not EWS or IMAP/SMTP - they both do not work)
  4. For login name, use something like jsmith01@tufts.edu (not John.Smith@tufts.edu)
  5. Chose OAuth as the authentication method
  6.  For OAuth, in the advanced options section provide Tufts Outlook Tenant ID: fbbf6c60-0344-4c29-9459-725685739b19
  7. Optionally configure Draft, Sent, and Archive folders to reside on the server. 

Hope this helps!

 


Wednesday, February 22, 2023

Computer Archeology: UMT (Ultimate Mail Tool)


Between 1993 and 1995, I've been leading a team at a software company in Kyiv, Ukraine, developing a mail client (MUA) with a graphical user interface for Unix (Irix, HPUX, Solaris, and Linux). It was an in-house, build-from-scratch product with the hope of selling it as a commercial offering. Back then, most Unix folks used text email clients, like elm or mutt, which lacked many modern features. In particular, the focus was on the following:

  1. International support (text encodings, fonts, etc.)
  2. MIME support (back then, sending binary attachments by inlining uuencoded text was still quite common).
  3. Rich text (bold, italic, multiple fonts, inlined images).
  4. S/MIME
  5. POP3/SMTP instead of reading local inbox and invoking `sendmail` to send out messages.


It sounds pretty trivial nowadays, but these features were missing from most Unix email clients on the market back then. The built-in address book and message filters were also quite innovative at the time. There were a few technical challenges as well. Since we wanted to be portable between various Unix flavours, we could not use SUN's Open Look, and the Motif toolkit had various portability issues between the platforms. We've chosen a not very well-known InterViews library (developed at Stanford University), which was very advanced for its time. It was in C++; everything was an object, had good Unicode support, etc. The C++ part was a plus but also a problem, as writing portable C++ code for HPUX, SGI, and GCC compilers was a challenge back then. As for network and email stuff, there were no existing libraries, and we had to implement POP3, IMAP, MIME, and related RFCs from scratch.


The project was a lot of fun. We were a small team of young software developers coding an exciting product on high-powered Unix workstations. We worked hard but found time for regular drinks and DOOM LAN parties at the office (often combined). Not surprisingly, the project failed commercially, but some people used UMT (Ultimate Mail Tool was how we named our product) for a few years after that.


Unfortunately, the source code was lost, but I found a copy of the web page (including screenshots) and some binary releases which I've published here, primarily for nostalgia reasons.

Friday, March 12, 2021

Importing mail from Google Takeout into another Gmail account

I had a Google Takeout export of my old University Google account, which I wanted to import into my personal Gmail. Unfortunately, Google does not provide an easy way to do this. I decided to use this as an opportunity to refresh my Haskell language skills, and in particular, to familiarize myself with the Pipes library. The idea was to process an arbitrary size mailbox in fixed memory without explicitly relying on Haskell's laziness. I will not bother you with details of my Haskell implementation. You can take a look at the code yourself, but take it with a grain of salt: I am not a practicing Haskell programmer. For me, this language is more of a lingua franca used in the academic functional programming community. I want to tell you about a few quirks and bugs of the Gmail IMAP interface I've discovered.

First of all, Google Takeout conveniently exports all your mail in standard mbox format as one huge file. Interestingly, this file also contains your chat transcripts, disguised as RFC822-formatted messages, but with the Message-Id field. They could be distinguished by the presence of the "Chat" label in the X-GM-Labels header field. I chose to discard them.

Speaking of labels: IMAP has folders while Gmail has labels. Gmail IMAP interface maps labels to folders. I use IMAP's STORE command and Gmail X-GM-LABELS IMAP extension to assign multiple labels to a single message.

Standard IMAP protocol (without UIDPLUS extension) does not give you a unique ID of a message you just appended. I need this unique ID to assign labels. So after successful message addition, I immediately look it up by Message-Id header field. At this point, I hit two bugs in Gmail IMAP implementation:

Bug #1

When Message-Id contains '%' character, the IMAP SEARCH command fails to find it. This a screenshot of this message present in my mailbox taken from the Gmail web interface:



But the following IMAP command fails to locate it:
UID SEARCH HEADER Message-ID "<D7DA993B.B30DC%psztxa@exmail.nottingham.ac.uk>"
Some people observed the same problem with "!" character and speculated that Gmail split message-id into "words" before indexing. The workaround proposed simulates this split and performs a search on the conjunction of several parts of the subject and then verifies that the found message has the correct Message-Id by fetching it. Instead, I chose to implement a more lightweight solution using X-GM-RAW Gmail's extension to IMAP's SEARCH command, which allows searching using google search syntax. In particular, for the example used above, one can use 
 
"Rfc822msgid:<D7DA993B.B30DC%psztxa@exmail.nottingham.ac.uk>" 
 
search query, which successfully finds the message with "%" in Message-Id.

Bug #2

Another Message-Id-related bug I've stumbled upon is more surprising. It turns out, when indexing messages, Gmail strips square brackets from Message-Ids! If you look at the screenshot from the web interface, you can see that Message-Id shown in the header does not match the actual field value below! To search for such messages, I had to strip square brackets in the search string.


Conclusion

This exercise is not a production-ready script, and some other problems may occur during the import, but I was able to successfully import my mailbox with about 32K messages. You are welcome to hack my script for your own needs. I've submitted a pull request for HaskellNet library with my bugfixes and changes to support Gmail IMAP extensions.
 
P.S. Both bugs were reported to Google: #183687621 and #183677218.




Tuesday, October 20, 2020

My computer setup

In this post, I will share how my 2020 computer setup looks (hardware and software). It will be interesting to read this in a few years to see how things may have changed.

Hardware:

I do 100% of my work on my laptop without using an external keyboard, monitor, or mouse. This gives me maximum portability. I can work anywhere: in a cafe, on an airplane, at the desk or on a sofa. My laptop is DELL XPS-13, which is very slim and lightweight. It is great for travel, and I have it in my backpack pretty much wherever I go. Performance-wise (I am doing a lot of compiling), it is pretty decent with i7 CPU, 16Gb of RAM, and SSD. Display quality is important to me, and Dell's 4920x2160 built-in HDPI display is very sharp and bright. I am not very happy with the keyboard and the touchpad, but I can live with it. The only external hardware I occasionally use is a 23-inch external monitor in portrait mode. I use it for convenience when I work on papers to preview my writing, showing a full page of LaTeX-generated PDF.

Software:

I am using the Ubuntu LTS release. I know there are cooler/more open Linux distros, but I need to balance tweaking my OS and getting actual work done. My hard drive is encrypted, in case my laptop is lost of stolen.

I am using `i3` window manager. It took me some time to customize it the way I want it to behave, but since I've switched to it was the most significant recent software-related productivity improvement. Virtual screens, keyboard shortcuts, efficient use of screen real estate allows me to be very productive.

I am using a `fish` shell. I like its interactive features and nice look-and-feel I have carved for myself using `omf` packages. However, I do not use it for scripting. In rare cases, when I need to do shell scripting, I use `bash.`

For almost three decades, my text editor is `emacs.` I am using many emacs packages, but if I have to name a few which I use the most, they are `helm,` `magit,` and `org-mode.` I use a solarized dark color theme in emacs, shell, and window manager.

My web browser is Firefox. Among a few extensions I use, `LastPass` is worth  mentioning.

Media processing:

At my home office I have a separate Mac Mini with 28-Inch 4k UHD Monitor, which I use solely for photo and video processing and video conferencing (due to "nose cam" on my Dell Laptop). The media processing software I use is Adobe Lightroom (standalone version) and Apple iMovie.

P.S. I may write a follow-up post about online services I use.



Wednesday, February 6, 2019

Switching between 3 languages with i3

I type in 3 languages: English, Ukrainian, and Russian. It turns out, I never have to switch directly between Russian and Ukrainian. However, when typing in either Russian or Ukrainian I often switch to English to type email addresses, URLs, Unix commands, etc. In such scenario using standard X11 keyboard switching mechanism with setxkbmap specifying all 3 languages is impractical. It cycles through them sequentially! For comparison, MacOS handles this situation nicely with cycling only through the last 2 most recently used keyboard layouts. I already posted a solution for standard Ubuntu window manager, but now I wanted to make it work with i3 window manager.

The idea is to have two typing models "us/ru" and "us/ua". You can switch between them using a key combination. Within each mode, you can switch between the languages using Alt+SPACE (or another key).



First, download this script and copy it into your ~/bin/ directory. Then add the following 3 lines to your ~/.config/i3/config:

bindsym Mod1+space exec "xkb-switch -n; pkill -x --signal=SIGUSR1 i3status"

exec_always "setxkbmap -layout us,ru -variant ,mac"

bindsym $mod+z exec "~/bin/cycle.sh /dev/shm/kbd2.txt 'setxkbmap -layout us,ru -variant ,mac' 'setxkbmap -layout us,ua' ; pkill -x --signal=SIGUSR1 i3status"

This is assuming you are using i3status keyboard indication method described in my previous post. Using it will also get the instant status bar update of the current keyboard languages. If you do not use i3status or do not need keyboard indicator you can use the following 2 lines instead:

exec_always "setxkbmap -layout us,ru -option grp:alt_space_toggle 

bindsym $mod+z exec "~/bin/cycle.sh /dev/shm/kbd2.txt 'setxkbmap -layout us,ru -variant ,mac -option grp:alt_space_toggle' 'setxkbmap -layout us,ua -option grp:alt_space_toggle'

Now you can use WindowsKey+Z to switch between "us/ua" and "us/ru" modes and Alt+SPACE to switch between en and either ru or ua layouts.